The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

>>>>> Eric Mullen 
>>>>> <emullen AT cs.washington.edu>
>>>>>  writes:

> 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?

Take two types from another programming language that *should* be isomporphic,
and use Coq to prove the isomorphism.  Even when I'm not "programming in Coq",
I use Coq as a testbench for proving that my Haskell types fulfill their type
class laws quite often.

This shows not only that Coq is a tool for reasoning that you can trust, but
that you needn't sell the farm to make practical use of Coq right away.

John