Interesting implementation strategy: it’s written in SPARK, an Ada subset oriented towards formal verification. Nice to see some of the tooling from that corner of the software-engineering world coming over to general-purpose systems programming, instead of only being used in aviation and medical applications.
I took a good look at the source for this some months back. It is indeed an awesome piece of work. Muen makes use of the intel VT virtualisation extensions to ensure separate kernel instances are mapped to different processors. Under the hood the code is extremely clean and well-written, and a great example of Ada’s many advantages as as embedded software language.
Interesting implementation strategy: it’s written in SPARK, an Ada subset oriented towards formal verification. Nice to see some of the tooling from that corner of the software-engineering world coming over to general-purpose systems programming, instead of only being used in aviation and medical applications.
I wonder if there’s a formally verified SPARK compiler to compile it with…
I took a good look at the source for this some months back. It is indeed an awesome piece of work. Muen makes use of the intel VT virtualisation extensions to ensure separate kernel instances are mapped to different processors. Under the hood the code is extremely clean and well-written, and a great example of Ada’s many advantages as as embedded software language.