5 ms·

Writing correct code, part 1: whatever happened to invariants?

49 points by MikeTaylor 16y ago

eru 16y ago
The beauty of Haskell and other languages with a powerful type system is, that you can express a lot of invariants with the type system. E.g. it is possible to express the Red-Black-Tree invariants in Haskell's type system.
lsb 16y ago
Invariants are still here. Instead of talking about them in comments, you can have automated test-generation via QuickCheck: http://haskell.org/haskellwiki/Introduction_to_QuickCheck http://haskell.org/haskellwiki/Introduction_to_QuickCheck
barrkel 16y ago
The irrelevant and distracting pictures of food on this blog are really starting to annoy me. I wish the irrelevant picture URL was more predictable, such that it wouldn't accidentally conflict with e.g. a graph or diagram.
- orborde 16y ago
  I find them something of an endearing quirk. They're like an inside joke for me, now that I've read a lot of reprog posts.
  - dreaming 16y ago
    They give the blog a bit of charm, its nice
  - barrkel 16y ago
    When I see a picture of a nicely seared rare steak, my mind wanders to nice meals I've had, places I've been, etc. The distraction effect is almost akin to having a picture of a nude woman.
_pius 16y ago
Nice article. There's been a backlash against formal correctness and verification in software, but fundamentals like asserting (or even just writing) invariants can make almost everyone's code better.
alexgartrell 16y ago
Denote preconditions, postconditions, and invariants during interviews! It'll save your life when it comes to quickly finding the "off-by-one" bugs that tend to be problematic when you're reinventing strcspan or another C string manipulation function, or doing some crazy recursion. In real life, whenever I'm writing complex C functions, I always denote my preconditions, postconditions, and invariants. I also tend to denote non-obvious pre/post conditions above the functions, to optimize for the case of source-diving (when someone's just glimpsing around and trying to get the gist).
WildUtah 16y ago
This is my favorite sushi blog and the programming content is worth reading sometimes, too.
RiderOfGiraffes 16y ago
Lovely article about a simple technique that can be used to prevent a lots of bugs, and assist in the generation of correct code. Interesting that his code still has a (probably never triggered) bug. EDIT: Actually, looking at the exchange in the comments, the bug I thought it has, isn't. The code is right, but for a subtle (to me) reason that isn't clear (to me) from any of the comments, the code, or the invariant. Even more interesting than I thought.

49 points by MikeTaylor 16y ago

eru 16y ago

The beauty of Haskell and other languages with a powerful type system is, that you can express a lot of invariants with the type system. E.g. it is possible to express the Red-Black-Tree invariants in Haskell's type system.

lsb 16y ago

Invariants are still here. Instead of talking about them in comments, you can have automated test-generation via QuickCheck: http://haskell.org/haskellwiki/Introduction_to_QuickCheck http://haskell.org/haskellwiki/Introduction_to_QuickCheck

barrkel 16y ago

The irrelevant and distracting pictures of food on this blog are really starting to annoy me. I wish the irrelevant picture URL was more predictable, such that it wouldn't accidentally conflict with e.g. a graph or diagram.

orborde 16y ago
I find them something of an endearing quirk. They're like an inside joke for me, now that I've read a lot of reprog posts.
- dreaming 16y ago
  They give the blog a bit of charm, its nice
- barrkel 16y ago
  When I see a picture of a nicely seared rare steak, my mind wanders to nice meals I've had, places I've been, etc. The distraction effect is almost akin to having a picture of a nude woman.

_pius 16y ago

Nice article. There's been a backlash against formal correctness and verification in software, but fundamentals like asserting (or even just writing) invariants can make almost everyone's code better.

alexgartrell 16y ago

Denote preconditions, postconditions, and invariants during interviews! It'll save your life when it comes to quickly finding the "off-by-one" bugs that tend to be problematic when you're reinventing strcspan or another C string manipulation function, or doing some crazy recursion. In real life, whenever I'm writing complex C functions, I always denote my preconditions, postconditions, and invariants. I also tend to denote non-obvious pre/post conditions above the functions, to optimize for the case of source-diving (when someone's just glimpsing around and trying to get the gist).

WildUtah 16y ago

This is my favorite sushi blog and the programming content is worth reading sometimes, too.

RiderOfGiraffes 16y ago

Lovely article about a simple technique that can be used to prevent a lots of bugs, and assist in the generation of correct code. Interesting that his code still has a (probably never triggered) bug. EDIT: Actually, looking at the exchange in the comments, the bug I thought it has, isn't. The code is right, but for a subtle (to me) reason that isn't clear (to me) from any of the comments, the code, or the invariant. Even more interesting than I thought.