logoalt Hacker News

ch4s3yesterday at 6:08 PM3 repliesview on HN

How does contract programming differ from refinement types?


Replies

prydtyesterday at 6:16 PM

The contract programming in D is pretty much syntactic sugar for placing asserts at different parts of your program.

Refinement types can be used as compile time checks for preconditions and postconditions, while this contract programming is inserting runtime checks.

Here's a good post on the type state pattern in Rust (we don't actually have refinement types in something like Rust but the type state pattern is somewhere closer to refinement types on this spectrum): https://cliffle.com/blog/rust-typestate/

show 1 reply
xorvoidyesterday at 6:19 PM

Poor man's runtime "dynamic" version. AKA: A much worse version.

In advanced cases, you'd need dependent types, but the only place where that almost shows up is in the "amount <= balance" assertions. That's also silly because if you typed "amount" and "balance" correctly, then "balance -= amount" has to produce a runtime error because the resulting balance would be negative and not a valid value for the type. So, it's a very natural place anyway to force the programmer to properly handle errors anyways.

"Contracts" has been around a long time and has not caught on. That's usually a good sign that better approaches are prevailing.

In other words: refinement types are a better solution.

show 2 replies
bryanlarsenyesterday at 6:13 PM

The various contract proposals for Rust are used as input to both formal verification tools as well as input to the optimizer. A good example of one such tool that could utilize contracts is cargo-anneal (https://crates.io/crates/cargo-anneal)