Research

Verification is usually an afterthought in programming language design. It doesn't have to be. The more a programming language guarantees, the less there is left to prove.

Philip Wadler argued in 1990 that linear types can change the world, but it wasn't until Rust that they did. In safe Rust, a mutable reference gives exclusive access to the value it borrows. A proof can rely on that guarantee without separately proving that other references cannot interfere with an update. If the borrowed value is a counter, for example, we can focus on showing that an increment adds exactly one without overflowing.