I am just starting out with the ironclad kernel and the gloire OS built on top of it [1,2]. From the web page: "Ironclad is a formally verified, real-time ca

I am just starting out with the ironclad kernel and the gloire OS built on top of it [1,2]. From the web page: "Ironclad is a formally verified, real-time capable, UNIX-like operating system kernel for general-purpose and embedded uses. It is written in SPARK and Ada, and is comprised of 100% free software." I recall AdaCore working with Ferrous Systems a while back. Did anything come of it for rust? I believe one of the non-starters is rust does not have a formal standards specification like C, Common Lisp, or other PLs. It's hard to develop formal verification systems for a moving target. SPARK has formal verification tools and a legacy of high-integrity applications. The Ironclad kernel is progressing towards a substantially, formally verified kernel written in SPARK. Gloire is an OS implemented on top of Ironclad for PoC. I have sort of given up on rust, because I just don't find it enjoyable. I am working with Zig. This would be a good direction for Zig to take. Glad to see the effort here. I'll have to check it out a bit more. [1] https://ironclad.nongnu.org/ https://ironclad.nongnu.org/ [2] https://github.com/Ironclad-Project/Gloire?tab=readme-ov-file https://github.com/Ironclad-Project/Gloire?tab=readme-ov-fil...