Hacker News new | past | comments | ask | show | jobs | submit login

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.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: