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.
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...
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.
A lot of modern programs never terminate and thus to me "halting" means no longer able to compute, i.e it's hung/deadlocked.
Computer Science historically being seen as a gateway to software development has done a large disservice to both fields.