A Few Good Ideas in Programming Languages

I really like flow-sensitive type inference but it’s very easy for it to either become incredibly computationally expensive or end up with massive union types.

Borrow checking is that start of a good idea but coupling it with a region abstraction to avoid having escape hatches for every data structure that isn’t a tree can improve it a lot (again, it can end up being very expensive).

Contracts cover a large design space. C++26 explores most of the undesirable parts. But Verus (Rust) is a really good contract system that adds ghost state that lets you prove quite rich properties about a system. I’d love to see something inspired by it incorporated into a future iteration of Rust. The other extreme (which is differently useful) is found in Erlang: Erlang’s guard clauses give you overload resolution that follows the rules of a subset of the language, which lets you not just enforce preconditions but the optimise if they’re true and fall back to slower code otherwise.

Racket also has extensive support for contract programming. In my compilers course, my group used it to validate the entire test suite upon each individual pass, for as-we-went-along regression testing.

I find contract programming interesting in how it contrasts to gradual typing. Like gradual typing, it provides a partial level of safety and guarantees. Unlike gradual typing, it loosens itself from whatever notion of a type is around, and lets you attach arbitrary predicates to functions.

Being not a huge fan of gradual typing (the performance improvements are pretty limited) in all languages besides TypeScript, I always reach for contract Racket over typed Racket.