Oh boy, it's this season again

> [0] it does, in programs where there's no unsafe sections, and the stdlib has those out of necessity. The road to NIH is paved with concerns for purity.

The thing "total absence of unsafe" thing is from a proof about the transitively safe form of Rust, which proves that a total lack of unsafe is *sufficent*, not that it is *necessary*. There is active, ongoing work to improve on this result: http://plv.mpi-sws.org/rustbelt/

In addition, even with the use of unsafe, it still constrains the unsafe behavior significantly - though this is only valid in combination with privacy, the stdlib uses them in concert in a responsible manner. This enables the language to have a considerably smaller TCB that required auditing. See also, http://huonw.github.io/blog/2014/07/what-does-rusts-unsaf...

> [1] such as hype

Here I agree with you - in particular, that the hypothetical security advantages of microkernels are moot without a security _model_ in which to evaluate them. For that reason, I am considerably more excited by seL4 (and by extension, Robigalia) - seL4 has a strong security model, a formal proof its spec satisfies that, and a formal proof (on ARMv6 so far, but more in progress) that the implementation - all the way down to the machine code - implements that faithfully. Pairing that with a userspace written in Rust, as Robigalia[3] seeks to, further aids the goal of building reliable systems. In addition, seL4 is a modern microkernel, with performant IPC at its core and far more minimal design than the (IMO rather Mach-like, or more maximal yet) Redox design.

> [2] which, as I recall (for the Java incarnation anyway, the one Sun was going to try on thin clients), while they did do away with invalid pointer accesses, remained vulnerable to all other categories of exploit; so below the line it was uncomfortable and didn't really help.

I will note that Rust's guarantees are considerably stronger: In particular, while Java does away with actual null pointer accesses, it retains null objects with much the same semantics (which Rust avoids via strict reference lifetimes and the Option<T> type - essentially the Maybe monad), data races (which Rust avoids via strict ownership in its type system), and - if you're referring to JavaOS - it predated Java 1.3, much less 1.5 which introduced generics, and thus would have had to be downcasting from Object and so forth, introducing runtime type errors.

Beyond that, I do broadly agree with you that the state of microkernels has advanced a long way since the first generation, and repeating the same mistakes doesn't advance the art so much.

But just as history has shown that the first generation of microkernels could not live up to their promises, it's also shown that humans are still fundamentally fallible, and that tools which help reduce error have measurable, and often significant, effects on real-world reliability. I certainly don't think either microkernels or Rust are a write-off as they are today (the whole L4 family is succeeding in the world as a foundation for real-time systems, and seL4 has provable worst-case execution time guarantees, along with confinement and resource isolation.)

[0]: NMF
[1]: NMF
[2]: NMF
[3]: https://robigalia.org