4 ms·

The seL4 microkernel generates C code from a formally-verified "executable specification" written in Haskell. They could instead generate Rust code that would e

The seL4 microkernel generates C code from a formally-verified "executable specification" written in Haskell. They could instead generate Rust code that would extra typechecks and might be closer to the Haskell specification. https://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4 https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...

hga 10y ago
As far as I know, The seL4 microkernel team generates C code by hand from a formally-verified "executable specification" written in Haskell. Which is then verified by analyzing the binary code and linking it back to the spec.