Comment

Comment by josephg

SeL4 is a capability based operating system toolkit, entirely implemented in C. The core operating system is just a few thousand lines of code. Its even mathematically proven to be bug free - which is totally insane.

It even uses a capability to allocate (assign) memory. So you typically have a microservice (userland process) in charge of memory on the whole system. Other processes get heap memory allocated to them by asking that service for it. (Though typically you'll allocate large blocks, and divide it up using a normal allocator).

parent josephg 1 year ago

Discussion

Live from the official Hacker News API

A modern reader for Hacker News · SvelteKit + Skeleton