But the problem of correct program construction does not go away. There is certainly a middle ground somewhere, beyond which proofs become too expensive for mos

But the problem of correct program construction does not go away. There is certainly a middle ground somewhere, beyond which proofs become too expensive for most users. For the sorts of systems I work on, the sweet spot is close to Haskell 98, for others it may well be Python (no types at all).