3 ms·
Which is why you use mathematics to write formally verified software e.g. in Coq. :) This whole "move fast and break things" philosophy should be unacceptable,
by fmap 9y ago
Which is why you use mathematics to write formally verified software e.g. in Coq. :)
This whole "move fast and break things" philosophy should be unacceptable, if you want people to trust in your new cryptocurrency/voting machine/etc, but try telling your investors that it'll take 5 years to develop the software instead of 5 weeks to "a first prototype" whose bugs and bad design decisions will haunt you forever...
- xfer 9y agoCoq extraction is not formally verified.
- fmap 9y ago1) It will be very soon: http://www.cs.princeton.edu/~appel/certicoq/ http://www.cs.princeton.edu/~appel/certicoq/ CertiCoq is a formally verified compiler from Coq to assembly (using Compcerts backends), not just an extraction to Ocaml/Haskell/Scala. 2) Extraction is not the only approach to verifying software with Coq (see Verifiable C, or Bedrock). In other proof assistants, e.g., in Isabelle or HOL extraction isn't even available and so other approaches are common. For a nice example look at the bootstrapping process of CakeML (https://cakeml.org/ https://cakeml.org/). 3) Even if it wasn't, the point is that the trusted base with verified software is tiny compared to anything else that people are actually using. "It's not perfect" is not an excuse if it is basically perfect in practice. See the Csmith paper ("Finding and Understanding Bugs in C Compilers", https://embed.cs.utah.edu/csmith/ https://embed.cs.utah.edu/csmith/) and what they had to say about CompCert.