There are various tools in the research world, but little real world use. Isabel... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		qznc on Sept 8, 2013 \| parent \| context \| favorite \| on: Quark: A secure Web Browser with a Formally Verifi... 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/) ATS - C with proof assistant (http://www.ats-lang.org/) KeY - Java with verification annotations (http://www.key-project.org/)

iso-8859-1 on Sept 9, 2013 [–]

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

300,000 lines of code, still unfinished.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact