Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to show off Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to show off Coq


Chronological Thread 
  • From: "John Wiegley" <johnw AT newartisans.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] How to show off Coq
  • Date: Fri, 30 Jan 2015 15:07:32 -0500
  • Organization: New Artisans LLC

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



Archive powered by MHonArc 2.6.18.

Top of Page