Showing posts with label invariants. Show all posts
Showing posts with label invariants. Show all posts

Friday, April 23, 2010

Effective ML

Yaron Minsky has giving great advice on effective ML lately. For my money, the single most important lesson is #3: make illegal states unrepresentable. There are so many benefits-- and I've seen the awful drawbacks of not following it.

Saturday, March 07, 2009

Cognitive dissonance and correctness

I don't pretend to be a psychologist, but I find the mental process of getting a program correct fascinating. It feels like the process goes something like this:
  1. Cognitive dissonance ("this can't possibly always work, can it?")
  2. Confronting the danger ("what might go wrong?")
  3. Questioning assumptions ("what am I assuming, and why do I need to assume it?")
  4. Codifying assumptions as invariants ("P")
  5. Pushing invariants through the program ("∀x. P(x)")
There are lots of techniques for #5, of course, and modularity helps make it manageable; e.g., defensively add in checks to enforce P so it's safe to assume.

But the interesting part to me is really the fact that, if you have the discipline to follow it through, it's precisely that queasy feeling that something might go wrong that eventually leads you to discover the program's invariants and ultimately to get the program right.

I mentioned this to Mitch, and he added "it's that recognition of danger (#1) that keeps us honest."