7 ms·
The most viable option today seems to be writing code in some language with strong formal guarantees (Agda, Coq) with extracting to Haskell/OCaml for generating
by dmytrish 13y ago
The most viable option today seems to be writing code in some language with strong formal guarantees (Agda, Coq) with extracting to Haskell/OCaml for generating C code from there.
That's the way seL4 was written.