4 ms·

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 to

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.

betterunix 13y 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 https://en.wikipedia.org/wiki/Altran_Praxis
- octo_t 13y 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/gg487498.aspx http://msdn.microsoft.com/en-us/library/windows/hardware/gg4... [2] Satisfiability Modulo Theories
- marshray 13y 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-at-microsoft-static-driver-verifier-and-prefast-for-drivers.aspx?Redirected=true http://blogs.msdn.com/b/dsyme/archive/2007/09/19/f-ocaml-job... http://msdn.microsoft.com/en-us/library/ff552808.aspx http://msdn.microsoft.com/en-us/library/ff552808.aspx
panic 13y ago
CompCert (http://compcert.inria.fr/doc/index.html http://compcert.inria.fr/doc/index.html) is a "real-world", optimizing compiler the core of which was written and verified using Coq.
- rwmj 13y 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.
  - betterunix 13y ago
    ...why not duplicate the effort as an open source project? Coq, ACL2, and PVS are all open source. Writing a C compiler is certainly not trivial, but it should not take a good programmer more than a few months to do so (including the time needed to learn Coq/ACL2/PVS).
    - jbapple 13y ago
      I think that really trivializes the tremendous effort the CompCert team put into that work. You don't just need to write a C compiler, or learn a bit of a proof assistant, you need to do the actual work of proving the compiler correct. This took person-years of time from people who already were Coq experts.
    - vilhelm_s 13y ago
      Formally verifying software takes much more time than just writing it, perhaps a factor of 10. For instance, the seL4 project[1] states that they used 2.2 person-years to write the kernel itself, and 20 person-years on the proof. Apparently the version of CompCert from 2007 (before any optimizations) took 2 person-years to write[2]. But some of those persons were pretty impressive. [1] http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf [2] http://memocode.irisa.fr/2007/leroy-compcert-memocode07.pdf http://memocode.irisa.fr/2007/leroy-compcert-memocode07.pdf
freyrs3 13y 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 http://www.cis.upenn.edu/~bcpierce/sf/toc.html
ecyrb 13y ago
Using Coq to verify PDF files (video): http://www.youtube.com/watch?v=CmPw7eo3nQI 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/XmonadInCoq.pdf http://www.staff.science.uu.nl/~swier004/Publications/Xmonad...
LilValleyBigEgo 13y ago
> Been eyeing Coq for a while
profquail 13y ago
Also worth checking out is Isabelle/HOL (another proof system): http://isabelle.in.tum.de/ http://isabelle.in.tum.de/ There are a bunch of examples in the Archive of Formal Proofs: http://afp.sourceforge.net http://afp.sourceforge.net And some tutorials: http://isabelle.in.tum.de/doc/prog-prove.pdf http://isabelle.in.tum.de/doc/prog-prove.pdf http://www-madlener.informatik.uni-kl.de/teaching/ss2011/svhol/svhol.html http://www-madlener.informatik.uni-kl.de/teaching/ss2011/svh... http://www.cse.unsw.edu.au/~cs4161/08s2/ http://www.cse.unsw.edu.au/~cs4161/08s2/
lelf 13y 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? ;-)

betterunix 13y 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 https://en.wikipedia.org/wiki/Altran_Praxis

octo_t 13y 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/gg487498.aspx http://msdn.microsoft.com/en-us/library/windows/hardware/gg4... [2] Satisfiability Modulo Theories
marshray 13y 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-at-microsoft-static-driver-verifier-and-prefast-for-drivers.aspx?Redirected=true http://blogs.msdn.com/b/dsyme/archive/2007/09/19/f-ocaml-job... http://msdn.microsoft.com/en-us/library/ff552808.aspx http://msdn.microsoft.com/en-us/library/ff552808.aspx

panic 13y ago

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

rwmj 13y 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.
- betterunix 13y ago
  ...why not duplicate the effort as an open source project? Coq, ACL2, and PVS are all open source. Writing a C compiler is certainly not trivial, but it should not take a good programmer more than a few months to do so (including the time needed to learn Coq/ACL2/PVS).
  - jbapple 13y ago
    I think that really trivializes the tremendous effort the CompCert team put into that work. You don't just need to write a C compiler, or learn a bit of a proof assistant, you need to do the actual work of proving the compiler correct. This took person-years of time from people who already were Coq experts.
  - vilhelm_s 13y ago
    Formally verifying software takes much more time than just writing it, perhaps a factor of 10. For instance, the seL4 project[1] states that they used 2.2 person-years to write the kernel itself, and 20 person-years on the proof. Apparently the version of CompCert from 2007 (before any optimizations) took 2 person-years to write[2]. But some of those persons were pretty impressive. [1] http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf [2] http://memocode.irisa.fr/2007/leroy-compcert-memocode07.pdf http://memocode.irisa.fr/2007/leroy-compcert-memocode07.pdf

freyrs3 13y 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 http://www.cis.upenn.edu/~bcpierce/sf/toc.html

ecyrb 13y ago

Using Coq to verify PDF files (video): http://www.youtube.com/watch?v=CmPw7eo3nQI 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/XmonadInCoq.pdf http://www.staff.science.uu.nl/~swier004/Publications/Xmonad...

LilValleyBigEgo 13y ago

> Been eyeing Coq for a while

profquail 13y ago

Also worth checking out is Isabelle/HOL (another proof system): http://isabelle.in.tum.de/ http://isabelle.in.tum.de/ There are a bunch of examples in the Archive of Formal Proofs: http://afp.sourceforge.net http://afp.sourceforge.net And some tutorials: http://isabelle.in.tum.de/doc/prog-prove.pdf http://isabelle.in.tum.de/doc/prog-prove.pdf http://www-madlener.informatik.uni-kl.de/teaching/ss2011/svhol/svhol.html http://www-madlener.informatik.uni-kl.de/teaching/ss2011/svh... http://www.cse.unsw.edu.au/~cs4161/08s2/ http://www.cse.unsw.edu.au/~cs4161/08s2/

lelf 13y 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? ;-)