>> You’re writing down a mathematical formula that describes the program’s behavior and using some sort of proof checker that’s going to check the correctness o

>> You’re writing down a mathematical formula that describes the program’s behavior and using some sort of proof checker that’s going to check the correctness of that statement The obvious flaw in that approach is that clearly the 'proof checker' can itself be vulnerable to human error. Any complex program is going to have many 'proof checkers' which depend on each other to verify different parts of the system; if any assumption about what constitutes a valid proof for any segment of the logic is wrong, then that would introduce a vulnerability in the same way as a regular programming bug would. So then the real question about the effectiveness of formal verification would be; given the same amount of development time, are incorrect assumptions introduced when writing the 'proof checkers' less likely than bugs introduced when writing regular programming code? Aren't programming bugs always caused by incorrect assumptions? What is it about formal verification which frees a complex system from the evils of incorrect assumptions? Incorrect assumptions about the proof or incorrect assumptions about the logic, what is the real practical difference?