Aiming for Correctness with Types

I read the whole article. (Not all the code, though -- I'm not quite so masochistic.)

In this article, Steve exercises commendable self-discipline when speaking about languages other than Rust. He lets the facts speak for themselves, and the facts are wholly eloquent (and damning) enough.

The thesis, that a good type system does not just "catch errors", but can and should be put to work to make good programs, is too often neglected by people who should know better.

The types in a program amount to another program, in a declarative, functional language that runs at compile time, and generates the program that will run. It produces a correct program, not by watching for mistakes, but by generating only correct code. The person who provides the types -- the library author -- has defined what a correct program using it can have in it, so the resulting program ends up with only those things, by arranging that the only way the parts fit together at all is when they are used correctly.

That puts more responsibility on the library author, and is only possible if the language is expressive enough to enable writing that compile-time declarative program. So, as we get languages that can express smart types, our standards for what makes a good library go up.

The standards of excellence for widely used Rust and C++ libraries are getting very high, making it increasingly harder to write bad code using them. Most of the value of Rust in helping to produce good code is in that support provided by library authors, and finally much less so by the borrow checker. C++ has to get along without borrow checking, but gets the full value of libraries ensuring correctness by construction.

This is why both Rust and modern-C++ coders often say that when their code finally compiles, it usually also works right.

I really enjoyed the depth and detail this article went into to make its point.