35 points AriFordsham 1 hour ago 2 comments
kodoman 48 minutes ago | parent
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.
samiv 7 minutes ago | parent
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.