[im_down_w_otp]

You can already do this with certain forms of type-level programming. We did it in the Rust-based OS we created atop seL4. It started out as using types to track setup processes and kernel objects at compile-time to bring some of the guarantees seL4 provides only at run-time, and also to provide guard rails to ensure that you're not accidentally creating unsecure systems using the tools seL4 gives you. After some exposure to doing this it became clear that we could also track memory allocations this way, so we created an allocator to do exactly that.

It basically ensures at compile-time that every allocation in the program will succeed given some expected usable footprint, which also has the benefit of ensuring that we kill the kernel/OS immediately at bootstrapping if the machine/environment doesn't have enough memory to make sure our proof-carrying code can meet its expectations.

One huge problem with this approach though is that it doesn't scale well. Where "scale" is in the dimension of revising your programs because the type-parameters tend to bleed all over the place and don't compose well/at-all. So, it's great if you're sure you've got your design locked-in, but it's kind of a nightmare if you're still prototyping & refactoring.