Every story and comment from the Hacker News API, in a layout borrowed from 2001.
A comment on Formalizing Text Editors in Coq. Parent comment
A few examples of large scale industrial projects using formal assistants:
seL4: A proven correct commercial OS used in billions of mobile devices.
CompCert: A proven correct C compiler used by Airbus for avionics software.
ARM: End-to-end verification of CPUs (https://alastairreid.github.io/papers/CAV_16).
There are many more.
There are no comments on this comment yet.
A few examples of large scale industrial projects using formal assistants:
seL4: A proven correct commercial OS used in billions of mobile devices.
CompCert: A proven correct C compiler used by Airbus for avionics software.
ARM: End-to-end verification of CPUs (https://alastairreid.github.io/papers/CAV_16).
There are many more.