Mostly Typed

For Hackers and Other Heretics

Experiences Building an OS in Rust

On Sunday, I’ll be presenting a paper at Programming Languages and Operating Systems (PLOS) on our experiences building Tock in Rust. While we (OS and language builders) often like to think of system and language design as separate problems, they are really not. Instead, language features or constraints often lead to very different system designs.

Read More »

The ALLOW System Call

It is common for drivers to share data with application via shared memory. For example, an application might need to pass a buffer to a network driver in order to read a packet.

Read More »

Cannot Declare Drop Types Statically

So far in Tock we have been allocating the chip and platform definitions statically by declaring them in static mutable Option variables. They are declared as None but on platform initialization, we replace their values with real values:

Read More »

Making GHC and cabal sandbox play nice

So you’re building something in Haskell. You’re most likely using GHC as your compiler, and almost certainly using cabal to manage package dependencies. If you’re up on all the hippest new features of cabal, you’re probably using sandboxes to make sure your project compiles reliably and can, e.g., depend on older or bleeding-edge versions of packages without affecting your global environment. Great!

Read More »