Hacker News Reader

Comment by hwayne | Hacker News Reader

> The developer is encouraged to think of the invariants before trying to prove that their implementation satisfies them. This approach to software development asks the programmer to consider side-effects, error cases, and data transformations before committing to writing an implementation. Writing the implementation proves the invariant if the program type checks.

I really wish more languages took this to the logical conclusion and implemented first-class contract support. It seems work on contracts stopped with Eiffel (although I've heard that clojure spec is _kinda_ getting there).

View on HN

Racket took the baton from Eiffel: https://docs.racket-lang.org/guide/contract-boundaries.html

Check out Dafny, Whiley, and Liquid Haskell.

Ada also supports contracts, as does .NET with code contracts.

Contracts are useless. They merely describe what you want your code to be, not what your code actually is. Just grab a pen and a piece of paper, and start proving things about your programs.

> Contracts are useless.

No, they are not.

1. If the code doesn't conform to the contract, it will fail on the contract boundary, with a well-defined error. If this is useless, then `assert` is also useless, which it is, of course, not.

2. With a sufficiently well-designed language and sufficiently smart compiler, you can move some contract checks to compile-time. See Racket.

3. If your language supports both static and dynamic typing, the contracts are a dual of static types, which lets you interface the static and dynamic parts of the code seamlessly and automatically (in both directions). Again, see Racket.

Meta: I wonder, why it's mostly static-typing proponents who aggressively evangelize, insult the other side, are 110% sure they're right even though there is no scientific evidence and so on. Could it be the bondage&discipline approach of static typing just appeals to people with a certain mindset, who are statistically more probable to engage in such behaviors, no matter the subject?

0. Trapping the error doesn't make your program any less wrong. I agree that `assert` is equally useless.

1. With pencil and paper, you don't need to wait for a smart compiler - you can get started proving things about your programs today!

2. I can totally see what's coming next: “Being wrong is dual to being right, so being wrong is another possibility worth exploring”. Right?

> Meta: (slander)

No comment.

Reply on news.ycombinator.com