The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

A very different tack would be to show a highly automated proof of a moderately complex program, like some of the examples distributed with Bedrock.

On 01/30/2015 03:01 PM, Eric Mullen 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