Ironclad is a formally verified, hard real-time capable kernel for general-purpose and embedded uses, written in SPARK and Ada. It is comprised of 100% free software, free in the sense that it respects the user’s freedom.
Version 0.5.0 has been released.
This release brings a lot of improvements to mainly the scheduling, time keeping, userland, and networking subsystems.
The easiest way to try Ironclad, either virtually or on real hardware, is to use a distribution that uses it – Gloire seems to be the recommended option.
Gloire is an OS built with the Ironclad kernel and using GNU tools for the userland, along with some original applications like
gwm. This repository holds scripts and tools to build the OS from the ground up.
I had never heard of this project before, but it seems incredibly cool.
The primary users of such an operating system… would be developers, its GPL3 so no it doesn’t respect its developer users, and so it will likely have very very few end users. Basically GPL working against itself and working against its own developers once they get embroiled in lawsuits trying to keep their code from being used (which is contrary to what most developers actually want anyway).
Also its written in ADA and SPARK…. most people aren’t going to saddle themselves with that unless they are getting paid. It certainly could have some applications in that domain, but again, hampered by the license.
Looking at the website, I don’t think they’re under any delusions about their place in the world.
What makes the GPLv3 a bad license for OS kernel? As you point out, ADA and SPARK (both heavily tied to Adacore) is probably a bigger turn off to devs then the software license.
It’s just the opposite. From an end user perspective, it doesn’t matter if it is GPL or cuck licensed. But from a developer perspective, only the GPL will protect you from your labour being stolen for free by Big Tech.
Another Spark/ADA kernel https://wookey-project.github.io/ewok/index.html#ewok-kernel
Thank you, I was not aware of that project.
I’ll try it out on a VM first!
I’m fortunate to have a long term $DAYJOB working with Ada on new projects. It’s an excellent general-purpose language that has been used in all kinds of application domains and is scalable from very small to very large projects. However, it shines as a high performance embedded and/or systems programming language.
That’s cool. 🙂
Ada is a language I keep thinking I would like, or should try. Any suggestions for resources for someone wanting to get into Ada?
The Ada user journal has nice articles on the language and ecosystem, plus plenty of links and resources.
Alire is a cargo-ish tool for Ada.
http://www.ada-europe.org/auj/home
https://alire.ada.dev
Awesome, thanks!
I would start by downloading two free PDF books:
“Safe and Secure Software – An Invitation to Ada 2012” from https://www.adacore.com/books/safe-and-secure-software and “Ada Distilled” from https://www.adaic.org/learn/materials/ .
Then you can try the online courses at https://learn.adacore.com . This site lets you edit and compile the exercises in your web browser.