[dh997]

The analogy is wrong because most all languages are Turing complete, and therefore equivalent despite paradigm and feature differences. The main reason seL4 was written in Haskell and again in C was to cross-verify behavior. C might be legacy ubiquitous, however it doesn't have to be the last word in shared library development by any means.

Any language which has a toolchain which produce flat binaries or use link scripts to specify sections can potentially be used for kernel and os dev. Bonus points for a toolchain which can compile itself.

There are kernels written entirely in Rust with some assembly glue. Others are writing production embedded domain-specific OSes in Haskell, OCaml, etc. for real, mission-critical systems right now and have been doing so for the last 5-10 years.

C inherently or inadvertently leads to giant codebases and subtle bugs when used too liberally, as opposed to higher-level, statically-compiled languages like Haskell and others.

The main issue with legacy code is how we choose to either keep investing effort in putting fingers into the levees or try something new in an incremental fashion.

PS: I would like to see Go get with it and support non-usermode, self-hosted and embedded development without including a giant, hard-to-port runtime in everything.

[cyphar]

> The main reason seL4 was written in Haskell and again in C was to cross-verify behavior.

seL4 was modeled in Haskell, then written in C. Then they used tools to verify that the Haskell models matched the C code.