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

[whoke]

I like the concept of "inevitable grittiness"! I think languages like Lean actually do a very nice job of pushing the grittiness out to the boundaries of your program. Everything else can stay pure, and in domains that are amenable to mathematical reasoning (compilers, DSP, etc) it feels like a natural fit. I don't think you have to go all in, either. I ported the compiler project I'm working on from TypeScript to Lean and recently spent a weekend making all the functions total and implementing a few basic theorems. On a basic level it feels like writing Haskell, but there's a lot more room to grow with it.