"The promise of the JVM failed not because of design, but because of buggy implementations. "
Well said. That happened everywhere from desktop to server to embedded. However, safety-critical side of embedded further supported your point by building real-time, safe implementations of JVM (or subset) designed for certification. There were also companies using Ada to get systematic protections against errors with one, Praxis, doing semi-automated proofs with their SPARK language. A JVM implemented in Ada, SPARK, and (where necessary) C/C++ might have been much safer.
"JITs and GCs are tremendously complex beasts, with implementations least amenable to verification methods relative to most other software projects. "
There's actually verified JIT's and GC's they can draw on. I doubt they will, though. History shows they'll go with a non-verified design followed by penetrate and patch.
"Rust's borrow checker is worthless for ensuring memory ordering and life cycle invariants of machine objects."
I've long pushed Abstract, State Machines (or languages based on them) to do this kind of stuff better. The work on memory models can be ported to something like Asmeta. The algorithms can be checked against them by solvers. Then, equivalent software and/or hardware comes out the code generator with more analysis/tests in case it messed up. I got excited seeing Galois was using ASM's for hardware/software verification recently. They'd be great for checking security of interpreters against software and hardware level issues.
"The most safe alternative and likely sufficient for 80% of use cases would be a message passing interface, afterall."
I haven't updated myself yet on advances in typing for that stuff. Pony's method for type checking might help here since it uses a capability-secure, actor model. Wallaroo also uses it for a high-performance database. So, it's not a slouch either.
Well said. That happened everywhere from desktop to server to embedded. However, safety-critical side of embedded further supported your point by building real-time, safe implementations of JVM (or subset) designed for certification. There were also companies using Ada to get systematic protections against errors with one, Praxis, doing semi-automated proofs with their SPARK language. A JVM implemented in Ada, SPARK, and (where necessary) C/C++ might have been much safer.
http://www.aonix.com/pdf/pico-web.pdf
https://www.adacore.com/books/safe-and-secure-software
"JITs and GCs are tremendously complex beasts, with implementations least amenable to verification methods relative to most other software projects. "
There's actually verified JIT's and GC's they can draw on. I doubt they will, though. History shows they'll go with a non-verified design followed by penetrate and patch.
"Rust's borrow checker is worthless for ensuring memory ordering and life cycle invariants of machine objects."
I've long pushed Abstract, State Machines (or languages based on them) to do this kind of stuff better. The work on memory models can be ported to something like Asmeta. The algorithms can be checked against them by solvers. Then, equivalent software and/or hardware comes out the code generator with more analysis/tests in case it messed up. I got excited seeing Galois was using ASM's for hardware/software verification recently. They'd be great for checking security of interpreters against software and hardware level issues.
"The most safe alternative and likely sufficient for 80% of use cases would be a message passing interface, afterall."
I haven't updated myself yet on advances in typing for that stuff. Pony's method for type checking might help here since it uses a capability-secure, actor model. Wallaroo also uses it for a high-performance database. So, it's not a slouch either.
https://www.ponylang.io/