Ironclad OS项目：用Ada语言构建Unix内核

如果你在寻找类Unix、POSIX兼容的实时内核，市面上有很多项目在尝试构建这样的系统。而Ironclad项目因其独特的技术选择而脱颖而出——它使用Ada编程语言及其可正式验证的SPARK子集。

Ironclad OS项目正在开发一个全新的类Unix操作系统内核，主要面向小型设备和嵌入式系统，并计划支持实时处理能力。为了增强安全性，该系统支持强制访问控制（MAC），这是一种大型组织级别的安全系统，正如美国国家标准与技术研究院所描述的那样。

目前市面上确实存在不少类似的项目。当我们在GitHub上搜索类Unix内核时，得到了横跨23页的222个结果。但Ironclad的与众不同之处在于，它既不是用C语言编写，也不像Serenity OS那样使用C++，更不像Redox OS那样采用Rust。它甚至没有选择其他现代类C语言，比如Drew DeVault在其Hare语言项目中开发的Bunnix。

相反，Ironclad选择了安全系统编程语言的鼻祖——Ada语言，以及其契约设计方言SPARK。开发团队正在为Ironclad内核进行形式化验证工作，尽管这项工作尚未完成。据我们了解，目前唯一其他经过形式化验证的内核是seL4微内核，如果Ironclad能够实现这一目标，将是一项重大成就。

由于单独的内核本身用途有限且缺乏吸引力，该项目还开发了一个运行在Ironclad内核之上的更完整操作系统，名为Gloire，这个名字取自法国1859年的开创性远洋铁甲舰。Gloire使用GNU工具构建，这意味着更好的传统Unix兼容性——开发团队甚至正在将MATE桌面环境移植到Gloire上。Gloire的C标准库mlibc来自Managarm项目。

可能得益于Rust语言的推动，Ada语言最近似乎获得了更多关注。今年早些时候，AdaCore兴奋地报告Ada重新回到了TIOBE排行榜前20名，并且至今仍保持这一位置。正如我们在2023年提到的，我们将此归因于开源工具链的存在：GNU Ada编译器GNAT。

虽然已故的伟大程序员尼克劳斯·维尔特并没有直接参与，但Ada的语法及其强类型特性明显受到了Pascal的启发。它与C语言家族截然不同，但这并非首个用Pascal家族语言编写的类Unix操作系统。

回到20世纪80年代初，这类项目曾经繁荣一时。多伦多大学用Concurrent Euclid开发了TUNIS，但除此之外还有其他几个项目。Apollo的AEGIS OS用Pascal实现；1988年，Apollo添加了System V和BSD UNIX兼容环境并将其重命名为Domain/OS，该公司后来被惠普收购。Elxsi的专有工作站运行EMBOS，这是一个用Pascal实现的非常早期的微内核风格设计。DEC的实验性Topaz微内核用Modula-2+编写，华盛顿大学的SPIN操作系统则使用Modula-3。来自INRIA的原始Chorus微内核操作系统最初用Pascal开发。Chorus后来被Oracle收购并开源，其内核被用于Sun长期取消的JavaOS项目中。

换句话说，在类Unix操作系统中使用Pascal和类Pascal语言有着令人惊讶的悠久历史，特别是在微内核领域——Chorus甚至早于现在作为苹果macOS基础的Mach。Ironclad的开发始于2022年，虽然听起来令人惊讶且意想不到，但Ironclad只是这一悠久而多样化传统中的最新成员。

Q&A

Q1：Ironclad OS有什么特别之处？

A：Ironclad OS的特别之处在于它使用Ada编程语言和SPARK子集开发，这是一种安全的系统编程语言。该项目面向小型设备和嵌入式系统，支持实时处理和强制访问控制，开发团队还在进行形式化验证工作。

Q2：Ada语言为什么适合开发操作系统？

A：Ada是安全系统编程语言的鼻祖，具有强类型特性和契约设计能力。它的语法受Pascal启发，与C语言家族不同。Ada语言最近重新回到TIOBE排行榜前20名，部分原因是有了开源工具链GNU Ada编译器GNAT。

Q3：历史上还有哪些用Pascal语言开发的操作系统？

A：历史上有很多Pascal家族语言开发的类Unix系统，包括多伦多大学的TUNIS、Apollo的AEGIS OS（后改名Domain/OS）、Elxsi的EMBOS、DEC的Topaz微内核、华盛顿大学的SPIN系统，以及INRIA的Chorus微内核等。