[geofft]

I assume the comparison is to environments like Coq, Agda, Isabelle/HOL, Idris, etc. But in most of those environments, there's still a distinction between the language itself and the proof assistant.

I would not be shocked if someone figured out a brilliant way to add dependent types to Rust 1.x within the next few years.

[rancur]

proofs are different from unit testing, right?

[geofft]

Yes. For instance, say you're implementing a red-black tree. In case your algorithms are as rusty as mine are: it's a particular form of binary tree where every node has a "color", red or black, the children of any red node are black, all leaves are black, and the count of black nodes from the root to any leaf (aka the "black-height") is the same. The intention is that the tree is roughly balanced by following these rules: the minimum height is the black-height (all black nodes), and the maximum height is double the black-height (alternating red and black).

You might want to check that the property "the number of black nodes from the root to any leaf is the same" is always valid. With unit testing, you'd implement the insertion and deletion functions, and write a unit test where you give them a few trees and make sure that the insertion and deletion functions don't break that property, probably by looping over every leaf and comparing the black-height. If this passes, you know that your functions are probably correct and at least not obviously broken, but you don't know that there isn't some edge case you haven't thought of.

With a language that supports proofs, you'd tell the compiler about the concept of black-height, and the type of a red-black tree would include the black-height. Therefore, in order to construct a valid red-black tree, you have to have constant black-height. Just as much as you couldn't construct a red node with a red child, you can't construct a node with two children of varying black-height. When you say that your insertion function returns a red-black tree, as part of type-checking, the compiler makes sure that these properties hold -- because in turn, every helper function you call, every constructor, etc. also requires these properties to hold so that they can return an object of type red-black tree.

The downside is that it's much more involved than a few randomly-selected test cases to convince the compiler that you're upholding the red-black tree rules in every single case. This textbook has an example of doing this in the Coq proof assistant (search for the section labeled "Dependently Typed Red-Black Trees"):

http://adam.chlipala.net/cpdt/html/MoreDep.html