Comment by incrudible

Neither of these examples answer my question: What's the point? Perhaps FizzBuzz is a terrible example for such a language, but I don't see anything being "proved" here. Can it do something like static asserts on the output, without actually running the program? E.g. can you prove that the outputs will never be anything else than "Fizz", "Buzz" or "FizzBuzz"?