Re:The SeL4 Foundation: What and Why
by qznc on Tuesday April 07, 2020 @07:30AM
(#22802254)
Practically every compiler does formal verification. The type checking of C for example. The question is what properties you want to verify. It isn't a binary question but rather a continuum from C up to Isabelle/Coq.
[ Parent
| on HN ]
Is it really formal verification if the type system is unsound? Due to undefined behavior, a "proven pointer-to-int" may not end up being a valid pointer-to-int at runtime. Even in Haskell, the type system is actually logically inconsistent (see http://okmij.org/ftp/Haskell/impredicativity-bites.html).