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.
Yes, but does it run Linu…
Oh wait, nevermind, at least until someone demonstrates Linux running under emulation. Then the answer will be “of course it does.”
doom?
“can confirm the code is going to do what we want under all possible conditions”
So, the polar opposite of modern AI-driven tools. Excellent. Diversity is good.
But I know which I’d pick to drive my car.
that’s… not what formally verified means. if at any point you think something “does what we want under all possible conditions” please pinch yourself, you’re dreaming.
Yeah, at best it means “some useful properties of the code can be proven”. For some basic algorithms you can prove the correct result and perhaps even in reasonable time, too, but for a whole OS? Nope.
In fact, the first thing you read if you go to their web is “Ironclad is a (partially) formally verified…”.
It may be put in lay mans terms but it’s not that far off. Silver mode means you can guarantee it won’t crash on any inputs. Higher modes mean that you can verify it will behave exactly to specification so not what you would want with hindsight but what you would want under envisaged circumstances (spec) (and warns you of problems for all possible inputs which you certainly couldn’t have thought of or fuzzed). You’re right that doing that for a whole general purpose OS would be quite a task but it’s certainly a good thing for the core systems. SPARK (Gnat prove is great). Proving can largely do away with a lot of testing to with much easier and better results. Gloire runs Mate desktop which is I guess written in C anyway of course.
“…under all possible conditions…”
Did you think about what that statement means before you hit publish?
That is a ludicrous claim, and not one made by anyone in that chain either.
That would mean the code is tested against situations like bitglips and other hardware shenanigans.
If it was restricted by hardware compliance and trustworthyness, it wouldn’t be “all” possible conditions would it?
Wtf is a “bitglip”, and why would autocorrect think it is a real word that “bitflip” should be changed to.
Sometimes tech just gets in the way…
Well ASCII f->g is a single bit flip, so put that down to the universe having a sense of humour…
In ASCII ‘f’ is 0b01100110 and ‘g’ is 0b01100111. So a bitglip is a bitflip (of bit 0), literally.
reminds me of my friend with a bad IDE cable, his computer on boot up would announce that it recognized his “CD-BOM” drive
I know on ATA disk drives, the Device ID sector has a signature at the end (0xA5) and also a modulo-256 check value. I would imagine ATAPI devices are similar in that regard.
Seems like his BIOS wasn’t verifying the integrity of what it got back from the drive…
I, for one, welcome our new bitglip overlords.
It’s just a typo. F and G are nutally adjacent on a QWERTY keyvoard. Let thy jets be cool. I understand it’s the fashion these days to blame autocorrect for one’s own tyoos.
That’s what we would need for the Raspberry Pi 1 these days!
A quick, small OS like RISC OS to run our experimental software.
I find this very exciting to be honest. I love Linux but good grief we have been living with Unix for a very long time. It is tired, tested, and proven but also old.
This plus Redox are kind of exciting to me. They both offer a chance to innovate. “Yes I know Linux/BSD/Unix has adopted innovations for a long time”. I would love to see these projects get more attention and developers. Maybe Redox could really use some better Video support and device support as I would think could Ironclad.