Rust is the new hotness in programming languages because of how solid its memory protections are. Race conditions and memory leaks are hardly new issues however, and as greybeards are wont to point out, they were kind of a solved problem already: we have Ada. So if you want a memory-protected kernel but aren’t interested in the new kids’ rusty code, you might be interested in the Ironclad OS kernel, written entirely in Ada.
OK, not entirely in classic Ada– they claim to use SPARK, too, but since SPARK and Ada converged syntax-wise over a decade ago, we’re just going to call it Ada. The SPARK toolchain means they can get this kernel “formally-verified” however, which is a big selling point. If you’re not into CS, that just means the compiler can confirm the…
Rust is the new hotness in programming languages because of how solid its memory protections are. Race conditions and memory leaks are hardly new issues however, and as greybeards are wont to point out, they were kind of a solved problem already: we have Ada. So if you want a memory-protected kernel but aren’t interested in the new kids’ rusty code, you might be interested in the Ironclad OS kernel, written entirely in Ada.
OK, not entirely in classic Ada– they claim to use SPARK, too, but since SPARK and Ada converged syntax-wise over a decade ago, we’re just going to call it Ada. The SPARK toolchain means they can get this kernel “formally-verified” however, which is a big selling point. If you’re not into CS, that just means the compiler can confirm the code is going to do what we want under all possible conditions — which is a nice thing to be able to say about the heart of your operating system, I think we can all agree. It’s a nice thing to be able to say about any code, which is one reason why you might want to be programming in Ada.
It’s also not something we can say without qualifications about Ironclad OS, as the verification process is still ongoing. Still, that lofty goal certainly sets Ironclad apart from other POSIX kernel projects.
Yes, the Ironclad OS kernel is POSIX compliant, like its Rust-based equivalent Redox OS. While it would be nice to see some innovation outside the POSIX box (outside of whatever Redmond’s doing these days), making the kernel POSIX-compliant certainly makes it a lot more useful. The Ironclad OS kernel is fully open source under GPLv3, with no binary blobs built in. The OSF will like that, and the rest of us should be able to tack on the binary blobs needed to run our hardware as usual, so it’s win-win.
They’re currently targeting RISC-V and x86, with test platforms being MilkV and LattePanda SBCs. If someone was willing to take on the project single-handedly, they could probably strongarm the project into supporting other architectures, if there’s are any other SBCs popular these days. PowerPC, perhaps?
For the supported architectures, there is already a usable (for some values of the word) distribution in the form of Gloire, which is appropriately named after the first ocean-going Ironclad vessel. The header image is a screenshot from an X-server on running on that distribution.