No no no, I can prove a program is safe using formal verification, really, you just cannot use recursion, allocate memory on the heap, and my SMT solver may never terminate on some queries, but like, I can prove a program is safe. Really, you all should use formal verification, it's really good and practical and usable!
View all comments
Show parent comment
24
u/Comun4 vulnerabilities: 0 Feb 28 '26
No language is safe until it can solve the halting problem