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.
Erlang guard clauses feel much more like (to me) like what I want out of a type system than what I usually get.
But tbf, mainstream PL are only starting to realise that pattern matching is good, so I am probably expecting too much of the Future to already be there.
Yup, I think the usability aspect is often overlooked. They aren’t more expensive than a lot of type systems but they don’t require a separate expression language and type language (or, rather, the equivalent of the type language is a subset of the expression language rather than a different thing). That’s a big usability win.
I haven't yet seen a compelling example of contracts (in D or C++) being significantly better than just "manually" adding the same checks. The Erlang functionality sounds kind of interesting and reminds me of the ability to overload by CPU capability in gcc. But most examples I've seen of contracts to me just look like a complicated way of doing the equivalent assertions in code.
I'd love to see an example that makes me "get" why having contracts is worth the complexity over just writing the code directly.
I don’t know that you will think this makes it “worth it”, as it is something that can be achieved manually with naming/comments, but in my mind the big value add over just adding the conditions “manually” is identifying whose responsibility it is that the conditions are met, which can be included in the information in the diagnostic, showing what code needs to be fixed to resolve a given violation.
contracts can be exposed as metadata in compiled libraries, which can improve codegen of calling functions and can help the compiler detect invalid arguments. (IIRC C++ contracts do this, which is a big part of the feature's complexity.)
class-level invariant contracts save a lot of boilerplate vs having to add the same postcondition to every non-const method.
Midori got good use of contracts for optimisation. Preconditions were inlined at the call site and were almost always optimised away, and then became assumes in the callee. The converse applied to postconditions. This is explicitly out of scope for C++ contracts.
Contracts written in a subset of the language that is amenable to static analysis can be a fantastic tool for formal verification. This is what Verus does. It is explicitly out of scope for C++ contracts.
Contracts that can be used for overload resolution are a great tool for extending the type system wi5 arbitrary dynamic dispatch to specialised implementations. This is explicitly out of scope for C++ contracts.
Contracts for API invariants are a less clear way of expressing interface properties than defining the interface in terms of types that make the undesirable states unrepresentable. This use case is in scope for C++ contracts.
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.
Borrow checking isn’t just for thread safety. It also prevents aliasing, which prevents certain bugs and helps the optimizer, and it’s a key part of tracking lifetimes.
Contract programming solves the problem at the wrong layer. An assert or an enforce only tells you an invariant broke after the program has already run the path that broke it. Dependent types push the same guarantee to the type checker, so a function like daysInFebruary returning 28 | 29 doesn't need an out clause at all; the return type is the proof.
The catch is that full dependent typing used to mean writing proof terms by hand, which is why Idris and Coq stayed niche outside a small circle of people willing to pay that cost. Worth a look if you haven't lately: Lean has made the practical case for dependent typing noticeably better since it showed up.
For the middle ground, refinement types (Liquid Haskell, F*, Dafny, and Verus which came up in this thread already) hand a lot of the predicates a contract would check to an SMT solver instead, statically, without asking anyone to write a proof term. That covers most of what class invariants and pre/post-conditions are doing in the article's BankAccount example.
One place I'd push back on any of these replacing contracts entirely: validating input that crosses the boundary from outside the program. That's not really a typing problem, dependent or otherwise. A user who fed in a bad value needs an error they can act on, not a type checker's rejection or a thrown exception a caller three frames up has to translate into something readable. Result/Either at the boundary, with the failure modeled as data, ages better there than either contracts or a fancier type checker.
I was not aware of enforce and I really like it! I frequently abuse assert statements because adding my own helper function seems incorrect. It feels like making a significant change to how programs are written that deviates from the language and standard library design.
david_chisnall | a day ago
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.
Diana | 21 hours ago
Erlang guard clauses feel much more like (to me) like what I want out of a type system than what I usually get.
But tbf, mainstream PL are only starting to realise that pattern matching is good, so I am probably expecting too much of the Future to already be there.
david_chisnall | 8 hours ago
Yup, I think the usability aspect is often overlooked. They aren’t more expensive than a lot of type systems but they don’t require a separate expression language and type language (or, rather, the equivalent of the type language is a subset of the expression language rather than a different thing). That’s a big usability win.
sdt | 16 hours ago
I haven't yet seen a compelling example of contracts (in D or C++) being significantly better than just "manually" adding the same checks. The Erlang functionality sounds kind of interesting and reminds me of the ability to overload by CPU capability in gcc. But most examples I've seen of contracts to me just look like a complicated way of doing the equivalent assertions in code.
I'd love to see an example that makes me "get" why having contracts is worth the complexity over just writing the code directly.
lcapaldo | 13 hours ago
I don’t know that you will think this makes it “worth it”, as it is something that can be achieved manually with naming/comments, but in my mind the big value add over just adding the conditions “manually” is identifying whose responsibility it is that the conditions are met, which can be included in the information in the diagnostic, showing what code needs to be fixed to resolve a given violation.
snej | 10 hours ago
david_chisnall | 8 hours ago
Midori got good use of contracts for optimisation. Preconditions were inlined at the call site and were almost always optimised away, and then became assumes in the callee. The converse applied to postconditions. This is explicitly out of scope for C++ contracts.
Contracts written in a subset of the language that is amenable to static analysis can be a fantastic tool for formal verification. This is what Verus does. It is explicitly out of scope for C++ contracts.
Contracts that can be used for overload resolution are a great tool for extending the type system wi5 arbitrary dynamic dispatch to specialised implementations. This is explicitly out of scope for C++ contracts.
Contracts for API invariants are a less clear way of expressing interface properties than defining the interface in terms of types that make the undesirable states unrepresentable. This use case is in scope for C++ contracts.
apropos | a day ago
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.
snej | 10 hours ago
Borrow checking isn’t just for thread safety. It also prevents aliasing, which prevents certain bugs and helps the optimizer, and it’s a key part of tracking lifetimes.
hongminhee | 16 hours ago
Contract programming solves the problem at the wrong layer. An assert or an
enforceonly tells you an invariant broke after the program has already run the path that broke it. Dependent types push the same guarantee to the type checker, so a function likedaysInFebruaryreturning28 | 29doesn't need anoutclause at all; the return type is the proof.The catch is that full dependent typing used to mean writing proof terms by hand, which is why Idris and Coq stayed niche outside a small circle of people willing to pay that cost. Worth a look if you haven't lately: Lean has made the practical case for dependent typing noticeably better since it showed up.
For the middle ground, refinement types (Liquid Haskell, F*, Dafny, and Verus which came up in this thread already) hand a lot of the predicates a contract would check to an SMT solver instead, statically, without asking anyone to write a proof term. That covers most of what class invariants and pre/post-conditions are doing in the article's
BankAccountexample.One place I'd push back on any of these replacing contracts entirely: validating input that crosses the boundary from outside the program. That's not really a typing problem, dependent or otherwise. A user who fed in a bad value needs an error they can act on, not a type checker's rejection or a thrown exception a caller three frames up has to translate into something readable.
Result/Eitherat the boundary, with the failure modeled as data, ages better there than either contracts or a fancier type checker.koala | 15 hours ago
I was not aware of
enforceand I really like it! I frequently abuse assert statements because adding my own helper function seems incorrect. It feels like making a significant change to how programs are written that deviates from the language and standard library design.