[ctenb]

Tangentially related, this post git me reading about the spectre language. In the spectre docs you write: "There is a notable lack of contract based programming languages that enforce correctness at a low level.". What is the difference between a function checking arguments and throwing exceptions and contract-based functions, apart from perhaps a more concise syntax to specify it?

[pizza_man]

The contract system allows for static propagation of trust throughout a program. If some given invariant can be assumed to hold true for the duration of a function, its clearer what can and cant happen (semantically, as opposed to doing try/catch everywhere, and then missing some blindspots, and then adding more try/catch to cover those blindspots, this is actually resolved two-fold in Spectre by using option[T]/result[T, E] on top of the trust/contract system). Moreover, type-level invariants are evaluated at compile time where possible, and non-guarded pre/postconditions are stripped from release builds for performance, meaning you can get the performance of no runtime checks and the safety guarantees (assuming you test before building with --release) provided by contracts.