I know that Proof Assistants can be used in fact-checking, but what else can they be used for? How would they be used for specific roles, including industry jobs and everyday life?
$\begingroup$
$\endgroup$
1
-
1$\begingroup$ Chapter 3 of the book "QED at Large" by Ringer and coauthors seem to have some nice examples $\endgroup$– Agnishom ChattopadhyayCommented Jun 14 at 21:03
Add a comment
|
7 Answers
$\begingroup$
$\endgroup$
2
A compiler called CompCert for the C programming language was released in 2005 (17 years ago!) and the proof assistant Coq was used to help program that compiler, as well as to help prove that it works.
Coq was also used in a formalization of the proof of the 4-color theorem which culminated in this paper published in 2008, though the theorem was proven with the help of computers (but without proof assistants!) decades earlier.
A more recent example was the formalization of the proof of the Feit-Thompson Theorem in September 2012, although the theorem itself had been proven without a proof assistant as far back as 1962.
-
$\begingroup$ How is the last example an example to what is being asked? With 4CT I understand a formal proof helped settle the skepticism people had towards its highly computational proof, but I don't think any such worries were present for Feit-Thompson. $\endgroup$– WojowuCommented Feb 8, 2022 at 23:18
-
3$\begingroup$ @taylor.2317 I don't quit see the point of accepting answers to "big list" questions like this. I think if nothing else it discourages others from posting their own answer. (I assume you were looking for more than one answer, and there certainly are many in this case.) $\endgroup$ Commented Feb 9, 2022 at 4:20
$\begingroup$
$\endgroup$
3
One of the great examples of Coq usage is SPIRAL, which has HELIX, a formally verified language and rewriting engine for generating high-performance implementations extracted from Coq proofs as optimal intrinsic multiplatform code (AVX, NEON, SSE, etc.). These extractions even came to Fortran libraries which are known to be super fast (mind that this assembly is extracted from Coq with SPIRAL). So whenever you run BLAS you're using code which was extracted by a proof assistant. Here is a recent paper SPIRAL: Extreme Performance Portability that provides a discussion of the SPIRAL system, its domain-specific languages, and code generation techniques.
-
$\begingroup$ I don't know BLAS implementations which use the code you mentioned. Most people run either the prototype NetLib implementation (no assembly code), or OpenBlas (hand-written assembly). There are also closed source implementations by hardware vendors, e.g. MKL by Intel. $\endgroup$ Commented Feb 12, 2022 at 15:55
-
$\begingroup$ Yes, you mentioned it right. It is Intel IP. $\endgroup$ Commented Feb 12, 2022 at 15:57
-
$\begingroup$ I contacted with co-author to enlighten the details: crocodile.org/lord $\endgroup$ Commented Feb 12, 2022 at 16:22
$\begingroup$
$\endgroup$
0
Fiat-cryptography uses Coq to generate verified, correct C code implementing cryptographic primitives. I believe it is currently used by some major web browsers.
$\begingroup$
$\endgroup$
Intel hired John Harrison, the creator of the HOL Light proof assistant, to formally verify the correctness of floating point arithmetic of Intel's chips (which you may recall had an embarrassing bug a few years prior). There is a nice story in this podcast about John showing through his formalization that one can do certain floating point operations with fewer chip instructions.
$\begingroup$
$\endgroup$
The seL4 microkernel (approx ~9000 lines of C) was verified in Isabelle/HOL. See this page for a discussion of just what this proof means (e.g., in terms of what assumptions underpin it). This code has been deployed by the likes of Collins Aerospace and Boeing as part of DARPA research projects.
The CakeML system is a verified compiler for a functional programming language that has proofs of correctness for every transformation from input strings to machine code, and bootstraps itself.
$\begingroup$
$\endgroup$
There's a verified TLS implemented in F* language: https://github.com/project-everest/mitls-fstar
F* is a dependently typed programming language with refinement type. Imo, it features in a tactic language for solving refinement constraints (so convincing the solver becomes less essential).
$\begingroup$
$\endgroup$
They are used a lot in software development, to verify correctness of implementations, as well as verifying correctness of database transactions protocols, and even to generate executable code (this is called program extraction). See Software Foundations
One proof assistant used for such tasks, apart from Coq, in the past 30 years, is PVS.
