On: Rust borrow and lifetimes

[pjmlp]

> Their runtimes are implemented in raw C or C++ and are not formally verified.

This is not true of all implementations. There are meta-circular implementations of Java and C# compilers, that people keep forgetting about.

[pcwalton → pjmlp]

Metacircular implementations still have a runtime underneath. You can't escape the need for formal verification if you want to be provably correct.

[pjmlp → pcwalton]

Yes, but it is simplified by removing a whole class of exploits C and C++ allow for.