Secure Unix ancestor KSOS did type safety before Rust made it cool

KSOS, a Unix-compatible operating system developed in the late 1970s and 1980s with US Department of Defense backing, used a type-safe programming language (Modula) and was designed for formal verification. Its source code, now publicly available via The Unix Heritage Society, highlights its modern security features and historical significance compared to contemporary systems like seL4 and Rust-based projects.