[kkowalczyk]

1. 3.8.0.2 fixed a logical error in the code. High-level language won't help you if you invert a logical condition or commit some more subtle logical mistake.

2. Our software also needs to be fast. No one needs a slow database engine. There is no high-level language that beats C on tasks like writing sqlite.

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.

Sqlite works. Testing works.

If there actually was a credible alternative to C for writing software that is efficient and reliable with requirements that sqlite has, I can assure you that people would use it. The problem is: it doesn't exist.

[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".

[qznc]

Contenders would be ATS and Nimrod. Neither fulfills the "one piece of widely used, reliable software that was written in it" requirement, though.

[adrianN]

Airbus planes run software written in Ada. Ada does fairly well in the programming language shootout and is designed for writing reliable software.