The Coq mailing list

[Matej Grabovský <mgrabovsky AT yahoo.com>]

As an aside, personally (as a CS undergrad), I believe that it would be beneficial to have such a simple, real-world example on the Coq homepage, or at least within a click's reach.

Matěj G.

On Friday, January 30, 2015 9:02 PM, Eric Mullen <emullen AT cs.washington.edu> wrote:

If you wanted to give a 10 minute demo to show off how cool Coq was, what example would you use?

Specifically, if you were talking to a bunch of undergraduates in Computer Science, and you had 10 minutes to convince them that Coq was an awesome research tool, what would be your go to example?

Ideas so far have been:

 * Implementing slow and fast Fibonacci functions, and proving they calculate the same thing

 * Proving that the identity function and the Fibonacci function are both monotonic

I'm leaning towards the second due to its simplicity, but I would very much appreciate small examples which illustrate how cool it is to write code and prove properties about it.

Thanks much,

Eric Mullen