I believe there's a hard distinction between abstract, mathematical correctness in software and functioning in the real world. Any software that's processing inputs and provides complex workflows to humans has to necessarily deal with the endless vagaries of reality.

That's not to say there isn't value in formal correctness, but the important part is identifying when it's useful and when its more trouble than its worth...

I was always interested in formal verification but have only written toy proofs and derived programs.

It's nice to see this older discussion of the topic outside of 'AI does lean' and the assumptions that formally verification is easy or will be easy for AI and you can just switch you brain off.

Build programs that can be verified in the first place is difficult design problem that requires real thought and deep insight of the problem.

The real question is: for a typical program we prove it - even though we know there are programs we can't prove?

I don't care about the examples given, I care about my word processor, web browser and such. Can we prove them - putting limits on the scripting language

Maybe it's just me but the terminology used in "halting problem" didn't age well.

A lot of modern programs never terminate and thus to me "halting" means no longer able to compute, i.e it's hung/deadlocked.

I adore that it has become normalized in vibe-coding circles to go "actually, maybe correctness doesn't exist! as long as it runs on my machine it's fine"

Only developers see software in it's full resolution. The rest of us see an abstraction; the sheet lying over the top of a device that will never actually be unveiled due to its grotesque appearance. The public can barely even handle the aesthetics of the sheet.

Management and marketing can only cope with a vague, third party description of the sheet.

[dead]