1) 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

1) 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.