[derefr]

> 3. Finally, show me that unicorn high-level language with strong, automatically provable invariants and one piece of widely used, reliable software that was written in it.

Not implying that this is true now, but this is the specific goal of Rust, with Servo.

[cwzwarich]

With its current design trajectory, Rust won't be able to prove interesting high-level invariants. It's going to give you the kinds of things you can prove with traditional ML-style type systems and affine types. The combination of the two lets you encode some interesting things, e.g. typestates, but they won't let you express something like "this browser engine correctly implements CSS".