> verifying software is correct implies solving the halting problem.
No, producing a program that can verify that all correct programs are correct implies solving the halting problem.
Verifying a particular piece of software is correct just implies you've proved that one piece correct. (And probably wasted your time dicking around with it only to find that the actual issue was in software you treated as 'outside' of the software you were verifying...)
No, producing a program that can verify that all correct programs are correct implies solving the halting problem.
Verifying a particular piece of software is correct just implies you've proved that one piece correct. (And probably wasted your time dicking around with it only to find that the actual issue was in software you treated as 'outside' of the software you were verifying...)