Distributed data structures with Coq

http://christophermeiklejohn.com/coq/2013/06/11/distributed-data-structures.html

by cmeiklejohn • 13 years ago

97 24 13 years ago

goldfeld• 13 years ago

Been eyeing Coq for a while, and this is fascinating and motivating for me to take it up (well, after Rust, Clojure and Racket, that is.) Can anyone point me toward projects or tutorials where Coq's proofs are used to build great practical real-world systems? My thinking is i'd love to delve into induction and logics while building something useful.

I just wish HN were more about this and less about "iOS7". Sometimes the amount of Apple zealots around here frightens me, who would support a company like that, and the NSA stuff sharing space with their stuff is quite a fit.

betterunix3• 13 years ago

I am not aware of Coq being used in the real world, but I have been told that Microsoft is using a similar tool in key parts of the Windows kernel (and that doing so has drastically reduced the number of BSODs people are seeing). There is also this company, though they are not using Coq per se:

https://en.wikipedia.org/wiki/Altran_Praxis

octo_t• 13 years ago

Microsofts driver development tool uses something called SLAM[1] to verify device drivers (which are the primary cause of system crashes), which uses Z3 as an SMT[2] solver.

SLAM basically models the NT kernel and the Win32 API and checks for loads of bugs.

[1] http://msdn.microsoft.com/en-us/library/windows/hardware/gg4... [2] Satisfiability Modulo Theories

marshray• 13 years ago

Static Driver Verifier, one of the early flagship projects for F#!

http://blogs.msdn.com/b/dsyme/archive/2007/09/19/f-ocaml-job...

http://msdn.microsoft.com/en-us/library/ff552808.aspx

panic• 13 years ago

CompCert (http://compcert.inria.fr/doc/index.html) is a "real-world", optimizing compiler the core of which was written and verified using Coq.

rwmj• 13 years ago

I love the idea at least of CompCert, but I really wish it was open source. I could drive adoption within Red Hat and in key open source projects tomorrow if it was.

freyrs3• 13 years ago

Depending on your definition of "real world", Benjamin Pierce (of TAPL fame) wrote a book about typing semantics using Coq. Of interest to compiler designers. http://www.cis.upenn.edu/~bcpierce/sf/toc.html

ecyrb• 13 years ago

Using Coq to verify PDF files (video):

http://www.youtube.com/watch?v=CmPw7eo3nQI

The core of the xmonad window manager was verified with Coq (PDF):

http://www.staff.science.uu.nl/~swier004/Publications/Xmonad...

profquail• 13 years ago

Also worth checking out is Isabelle/HOL (another proof system): http://isabelle.in.tum.de/

There are a bunch of examples in the Archive of Formal Proofs: http://afp.sourceforge.net

And some tutorials:

http://isabelle.in.tum.de/doc/prog-prove.pdf http://www-madlener.informatik.uni-kl.de/teaching/ss2011/svh... http://www.cse.unsw.edu.au/~cs4161/08s2/

lelf• 13 years ago

First verified (= you only have to trust coq small kernel) proofs of four color theorem and Feit–Thompson theorem is enough for real-world? ;-)

draugadrotten• 13 years ago

I am sorry, but "Coq" is competing right up there with "Megapussi" potato chips and "Wack off" insect repellant for the worst named product.

What on earth were you thinking naming it "Coq"?

http://www.oddee.com/item_96682.aspx

cmeiklejohn• 13 years ago

From: http://en.wikipedia.org/wiki/Coq

"The word coq means "rooster" in French, and stems from a tradition of naming French research development tools with animal names.[4] It is also a reference to Thierry Coquand, who developed the aforementioned calculus of constructions along with Gérard Huet. Also, at first it was simply called Coc, the acronym of calculus of construction."

deepblueocean• 13 years ago

I've always been convinced that the name is a cruel joke played on American computer scientists by their French counterparts.

betterunix3• 13 years ago

Do you also giggle at the name "Johnson?" I mean seriously, "cock" is widely used to refer to male birds. Yes, I would have laughed hysterically at this in middle school but we all have to grow up some time. Here is "cock" in an appropriate context:

At this stage of the chicks' development, the cocks usually has begun to enter the nest to help his hen in caring and feeding the chicks.

http://greatbudgies.webs.com/aboutbudgies.htm

"Cock" as a word is no different from "bitch" or "stud:"

https://en.wikipedia.org/wiki/Cock_%28bird%29

http://classic.akc.org/breeders/resp_breeding/Articles/carea...

https://en.wikipedia.org/wiki/Stud_%28animal%29

Mindless2112• 13 years ago

The name isn't doing the language any favors though. "I love Coq" isn't going to garner the same response as "I love Rust" despite how sincere you are about maturity.

_pius• 13 years ago

I take it you've never had Coq au Vin?

rdtsc• 13 years ago

How dare people from other countries not check with American sensibilities before naming their products.

We should perhaps invade them and teach a thing or two about American culture.

edwintorok• 13 years ago

Here are some interesting projects that use Coq proofs, I'll leave it up to you to judge how real world they are.

Generate OCaml code from Coq: https://github.com/msgpack/msgpack-ocaml/tree/master/proof

Proof algorithms written in OCaml using Coq: http://www.chargueraud.org/softs/cfml/

Write program specification and use multiple provers (including Coq): http://why3.lri.fr/

Write certified programs, and verify proofs using Coq: http://focalize.inria.fr/

Language semantics / type system proofs of languages: http://www.cl.cam.ac.uk/~so294/ocaml/ (for a subset of OCaml)

http://gallium.inria.fr/~protzenk/mezzo-lang/

Books on Coq: http://adam.chlipala.net/cpdt/ http://www.cis.upenn.edu/~bcpierce/sf/

doublec• 13 years ago

There's also the "Featherweight Firefox" browser model in Coq http://www.the-inconsistency-principle.com/upenn//browser-mo...

mjb• 13 years ago

I've experimented quite a lot with Coq, and am still struggling to get value from it in a distributed systems context. TLA+ (http://research.microsoft.com/en-us/um/people/lamport/tla/tl...), on the other hand, was useful to me from the first day that I tried to use it. It's model seems better suited to demonstrating properties of distributed systems, and often the exhaustive testing approach of TLC provides much of the same value that Coq's proofs do.

Coq and TLA+ obviously solve different problems, so comparing them directly isn't possible. For a first step into formal methods for distributed systems engineers, however, I'd recommend TLA+ based on my experiences.

Distributed data structures with Coq

Related Stories