nub
I’m in the first weeks of designing nub: Not Unix, Basically. The motto is “general-purpose, provably correct software, for everyone”. The idea is to build, on top of seL4, a software stack that builds compile time capability guarantees and other high-assurance primitives into every piece of software by default. “nub” is a good name because it can also be read as “noob”, which I am, when it comes to PL, type systems, and OS design. But I’m loving the deep connections that I am learning to draw across subjects like computability theory, functional programming, and brass-tacks software development. For example, I find myself understanding the purpose of the borrow checker in Rust (“to make race conditions impossible” is my understanding: feel free to correct me / add color). No website or GitHub repo yet. I’m brushing up on classical logic and learning Idris. Installed QEMU today.