Comment by bckr

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.