Last time we created a formally proven version of FizzBuzz, but it had some problems. Our proofs weren’t strong enough to prevent us making the version below, where anything divisible by five returns Buzz and everything else returns Normal. The problem is that we create proofs that a number is divisible but not proofs that […]
Tag: Proofs
Formally proving FizzBuzz for fun and profit, part 4.
Last time we created the data type FizzBuzzProofSimple, which represents possible FizzBuzz values and created a few instances of it by hand. The next step is to write a function for generating FizzBuzzProofSimple instances from any number automatically. Making Proofs First we’re going to need functions to make DivisiblebyX instances. These functions need to: Take […]
Formally proving FizzBuzz for fun and profit, part 3.
Last time we created a custom FizzBuzz data type and implemented the Show interface. The problem with our previous code was that the compiler wasn’t enforcing any correctness, so today we’re going to do that. Types are Proofs Types are proofs, being able to create an instance of a type, tells you something about the […]