tomjakubowski/fbaas — pull request #1 by jblake (2012-10-24 23:35:34+00:00)
Title: First run at a Coq+Haskell solution.

This solution uses Coq to construct a provably correct fizzbuzz function for single numbers at its core, then uses Haskell to slap a simple WAI/Warp-based HTTP server around it.

It's a little silly. Half the Coq code is just setting up the extraction environment; the "correctness" proofs boil down to 6 lines of Inductive definitions, and 8 invocations of the "auto" tactic. At some point I might see about lifting more of the parsing or range-handling code from Haskell into Coq, if only to make it look more impressive.

I have a Makefile for building the solution; you'll need coq and ghc and a recent version of the WAI packages, at least. I'm fairly certain this is correct; it compiles and runs for me, at least.

Presumably you'll want to make a new branch for this rather than merging into master; I can't work out how to make GitHub's pull request UI suggest that you do that.