In a hypervisor system, not even sure if that's possible.

It doesn't return anything about success or failure.

Yes.

Do you know what a microkernel is, and why they are so forcefully advocated?

I work at NICTA from time to time. Will raise this with them.

Haskell's garbage collection works (or should work) based on formal inference -- seeing as they translated the haskell to C manually, they would have proved the garbage collection as part of the deal. Also, haskell's prelude and basic libraries have already been formally proven.

Because of formal inference, a good Haskell compiler knows exactly when and what will be garbage collected at compile time - there is no mark-and-sweep approach like Java. It's no worse that manually freeing stuff in C, in fact it's substantially better.

L4 doesn't delegate memory management to a process, that is impossible, because it would then have to manage memory for the memory management process.

It would only kill the hardware it's dealing with, likely, so the kernel might still keep on chugging. All the kernel needs is memory and cpu after all :)

Thanks!

Malware would have a much harder time making a root exploit in this case.

Buffer overflows would've been solved by the haskell implementation. Assuming each of their C translations are free of overflows, the whole thing should be overflow free.

Do you know what "formal" means? It's talking about "formal" as in programs as formal systems, a branch of logicianship that allows you to reason about computation. I would much rather use a completely untested, but entirely formally proven operating environment than a long-lived unproven one. We just haven't gotten to the point where we have proved enough software yet.

Dude, can C's types be reasoned by formal inference? No. Hence, C does not follow typed logical calculus.

C doesn't follow boolean logic either, actually, it just maps to assembly instructions. The best thing you could do to reason about C is to use Dijkstra's proof method which is impractical in a large scale and easy to screw up.

no, Main is IO. putStrLn does not tell you if it was successful by returning a boolean.

1) L4 is a microkernel. You have no idea what you're talking about. If L4 works, then you could apply similar principles for all the other servers that run in kernel space.

2)This is the largest formal proof ever done in this sort of field. Seriously, the results are not immediately useful, but it's a good start.

Disclaimer: I have worked at NICTA in the past.