3 ms·
There are various tools in the research world, but little real world use. Isabelle/HOL - Coq competitor like GCC and LLVM (http://www.cl.cam.ac.uk/research/hvg
by qznc 13y ago
There are various tools in the research world, but little real world use.
Isabelle/HOL - Coq competitor like GCC and LLVM (http://www.cl.cam.ac.uk/research/hvg/Isabelle/ http://www.cl.cam.ac.uk/research/hvg/Isabelle/)
ATS - C with proof assistant (http://www.ats-lang.org/ http://www.ats-lang.org/)
KeY - Java with verification annotations (http://www.key-project.org/ http://www.key-project.org/)
- iso-8859-1 13y agoInterestingly, HOL Light is used to prove that the density of a packing of congruent spheres in three dimensions is never greater than pi/sqrt(18), a 400 year old problem: https://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet https://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet 300,000 lines of code, still unfinished.