尽管每个人（不包括我）都会告诉你，这个年代写新操作系统意义不大，然而谷歌还是隔三岔五地在折腾新的操作系统——钱多得花不完的大厂不止谷歌，为什么只有谷歌爱写新操作系统？

最近，谷歌某团队在博客上宣布了 KataOS 计划，值得注意的是它选用了 seL4 和 Rust。seL4 是目前唯一产业界公认可以通过形式化验证（目前仅限 ARM 平台可过测试）的操作系统内核，Rust 则是目前产业界幻想可以获得安全的语言——这听起来简直就是双剑合璧天下无敌。当然，这样的组合并不是什么全新的尝试，早在若干年前，某自动驾驶厂商就试图用 seL4 + Rust 的组合来给自己的下一代产品增加一些震撼人心的特性。很明显，倘若这样的组合真能够轻松征服世界，那么这家厂商就不再是“某自动驾驶厂商”了，但我们也许还是应该记住这位先行者的名字 Polysync。

实际上，谷歌在作出这样的计划前，也曾经考察过 Rust 当前 对于 seL4 的支持，不料却发现主要的支持库 seL4-sys（由 Polysync 开发且维护）早就不再活跃。并且 seL4-sys 的处理方式也不太合谷歌的胃口，它通过自动生成 seL4 函数的绑定来跟 Rust 对接。谷歌这么财大气粗讲究底层的公司，当然是通过汇编直接跟底层函数对接，这样无非就是不能像生成函数绑定那样跨平台，每个 CPU 平台都要写一组支持。但是这种多招几个工程师就能搞定的事情，对谷歌不叫事儿——尽管如此，目前主要还是支持了 RiscV。

作为微内核操作系统，安全方面主要就得靠 capabilities，对于 seL4 来说采用的是 capDL，一套方便定义 capabilities 的定制语言（DSL）。总体来说，seL4 本身确实比较激动人心，seL4 的问题也非常明显，那就是太小。而正是因为小（一万行左右的代码）才有机会完全通过形式化验证，问题也就来了，seL4 相当于一个小萝莉，你要基于她打造一个工业级的完整操作系统，需要大量的工程化。GNU 曾经讨论过是否用 L4 来替换 Mach 来构造下一代的 GNU Hurd，在讨论的时候第一个就淘汰的便是 seL4（seL4 是 L4 微内核家族的实现之一），因为要补充的部分实在太多了。这么来想像，即便你有一个完整的微内核，要打造一个像 GNU Hurd 这样的通用操作系统仍需极大量的工程化开发，而如果你选用了 seL4，那么光是先打造一个完整的微内核就需要大量工程化开发。

当然，谷歌有的是钱，这些都不是问题，问题在于计划的持续性，对吧 Fuchsia？谷歌会是那种长期坚持一个项目直到成功的那种公司吗？

大家自有结论。