RE: https://social.rust-lang.org/@rust/117605013073050966

I'm not sure whether I'm more excited about the stable never type, or DropGuard in std.

Which is a reminder that I'm kind of strange, since the word "allocator" didn't appear in that sentence. 🤪

@cliffle allocators are runtime type checking and we would be better off without them. (In system programming)

@Moore @cliffle I think this is a reasonable point of view, but I don't know if it's correct yet. What do you think about the seL4 approach to resource management?

@xentrac I have not worked with it but have been following it. It looks interesting.

@Moore I haven't tried installing seL4 either, but I mean, what do you think about its approach to resource management, in the abstract?

@xentrac I don't know enough to have an option but it looks interesting. The time accounting is interesting.

@Moore An interesting thing about that is that they only enable the time accounting for "mixed-criticality systems", where you're relying on the kernel to prevent your Linux virtual machine or whatever from causing glitches in your motor control waveforms or 802.11 acks.

But the main interesting thing about the kernel in this context is that it doesn't allocate memory at runtime. There's no heap.

@xentrac @Moore I don't know if I would look at it that way: another perspective is that it has first class heaps as capabilities. And method invocations analogous to calloc/free (but safe). After all, no kernel has a heap unless it implements it's own; this one is just ocap style

@tonyg @Moore Most kernels do implement their own heaps, though, while, as I understand it, seL4 leaves that to userspace. As a result, seL4 system calls cannot fail due to running out of memory. The kernel doesn't have a "heap" capability type, either. Maybe I'm not understanding what you mean.

@xentrac @Moore Ah, I see. Yeah the kernel cannot fail due to no-memory-available; allocation calls done by userspace can fail. It's a heap still, but the difference is that the kernel never calls those APIs. So I may have misunderstood the scope of your remark, in which case oops and I retract everything :) The capability type I am meaning is "Untyped".