14 ms·

> The developer is encouraged to think of the invariants before trying to prove that their implementation satisfies them. This approach to software development

by hwayne 9y ago

> 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).

bjz_ 9y ago
Check out Dafny, Whiley, and Liquid Haskell.
- naasking 9y ago
  Ada also supports contracts, as does .NET with code contracts.
greghendershott 9y ago
Racket took the baton from Eiffel: https://docs.racket-lang.org/guide/contract-boundaries.html https://docs.racket-lang.org/guide/contract-boundaries.html
catnaroek 9y ago
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.
- klibertp 9y ago
  > 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?
  - catnaroek 9y ago
    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.
    - klibertp 9y ago
      > No comment. But why? You were able to "comment" on the work of Felleisen and colleagues on contracts, declaring their effort of many years useless, yet you can't answer why did you do it? Your utter lack of respect for people who happen to hold an opinion different than yours is typical, in my experience, for static-typing fans; as is your apparent - and wrong - belief that static typing was proven to be "better" (for some value(s) of "better") than dynamic typing. There are certain groups of people where the above traits are overrepresented. I think there is a high probability that preference for static-typing correlates positively with belonging to these groups - and I wrote that much. Is that really a "slander"? Sorry for focusing on that part, but your 0-2 points are too wrong to correct in a few paragraphs, and I don't have the time for writing more than this.

by hwayne 9y ago

bjz_ 9y ago

Check out Dafny, Whiley, and Liquid Haskell.

naasking 9y ago
Ada also supports contracts, as does .NET with code contracts.

greghendershott 9y ago

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

catnaroek 9y ago

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.

klibertp 9y ago
> 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?
- catnaroek 9y ago
  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.
  - klibertp 9y ago
    > No comment. But why? You were able to "comment" on the work of Felleisen and colleagues on contracts, declaring their effort of many years useless, yet you can't answer why did you do it? Your utter lack of respect for people who happen to hold an opinion different than yours is typical, in my experience, for static-typing fans; as is your apparent - and wrong - belief that static typing was proven to be "better" (for some value(s) of "better") than dynamic typing. There are certain groups of people where the above traits are overrepresented. I think there is a high probability that preference for static-typing correlates positively with belonging to these groups - and I wrote that much. Is that really a "slander"? Sorry for focusing on that part, but your 0-2 points are too wrong to correct in a few paragraphs, and I don't have the time for writing more than this.