Comment by vessenes

I think it's worth putting a Knuth quote up on your board when you think about verification as an end goal: "Beware of bugs in the above code; I have only proved it correct, not tried it."

Or, as Wolfram proposes in another link on the front page today, the irreducibility of computation means we cannot generally get all bugs out of systems.

To my mind, one of the risks of going all in on verification is that you just move the difficulty to a harder, more abstract layer - the specification. In my experience, this typically looks appealing to a 'type' -- very high IQ, very little real world engineering experience -- it's a dream that hits the inevitable grittiness of the real world and .. the real world keeps winning.