Last time we made a function for determining which FizzBuzz variant is needed for a single number. Now we need calculate FizzBuzz for all the numbers between 1 and 100, then print them out. Note, Idris uses monads to perform IO such as printing to stdout. If you don’t know what monads are, good luck. […]
Category: FizzBuzz
Formally proving FizzBuzz for fun and profit, part 5.
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 […]
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 […]
Formally proving FizzBuzz for fun and profit, part 2.
Last time we introduced FizzBuzz and the Idris language. The problem with our last solution (shown below) was that it combined determining what the output should be with actually creating the output strings. This time we’ll be fixing this by add Algebraic Data types and Interfaces. Algebraic Data Types Algebraic data types are types composed […]
Formally proving FizzBuzz for fun and profit, part 1.
FizzBuzz is a programming problem often used as a trivial coding interview challenge to filter out the programming job candidates who can’t program. It is defined as follows: Write a program that prints the numbers from 1 to 100. But for multiples of three print “Fizz” instead of the number and for the multiples of […]