Rust因其可靠的内存保护机制成为编程语言界的新宠。然而竞态条件和内存泄漏并非新问题，正如资深开发者常指出的，这其实早已有了解决方案：我们拥有Ada语言。因此，如果您想要一个具备内存保护功能的内核，却又对新兴语言的代码不感兴趣，那么完全用Ada编写的Ironclad OS内核可能会引起您的关注。

严格来说，它并非完全使用经典Ada——开发团队声称还使用了SPARK，但由于SPARK与Ada在语法层面已于十多年前融合，我们不妨统称为Ada。SPARK工具链使得该内核能够实现“形式验证”，这是个重要卖点。对于非计算机专业背景的读者而言，这意味着编译器可以确认代码在所有可能条件下都会按预期执行——对于操作系统的核心部分来说，这无疑是值得追求的特性，相信大家都会认同。实际上，这是所有代码都期望具备的特性，也是您可能选择使用Ada编程的原因之一。

不过，对于Ironclad OS而言，这个说法还需要附加说明，因为验证过程仍在进行中。尽管如此，这个崇高目标确实让Ironclad在其他POSIX内核项目中脱颖而出。

与基于Rust的Redox OS类似，Ironclad OS内核也符合POSIX标准。虽然我们乐于看到在POSIX框架之外的创新（不论微软最近在做什么），但保持内核的POSIX兼容性确实能显著提升其实用性。Ironclad OS内核基于GPLv3协议完全开源，且不包含任何二进制闭源组件。开源基金会会欣赏这一点，而普通用户仍能按需添加硬件所需的二进制组件，实现双赢局面。

该项目目前主要支持RISC-V和x86架构，测试平台为MilkV和LattePanda单板计算机。如果有人愿意独立承担移植工作，或许能推动项目支持其他架构——如果现在还有其他流行的单板计算机的话。比如PowerPC？

针对已支持的架构，项目提供了名为Gloire的可用发行版（在特定定义下可用），这个名字恰如其分地取自首艘远洋铁甲舰。文章顶部图片正是运行在该发行版上的X服务器截图。