A general-purpose program to verify software functionality is undecidable
What sorts of problems are undecidable by computer? Are they esoteric, dwelling only in the minds of theoreticians? No! Even some ordinary problems that people want to solve turn out to be computationally unsolvable. In one type of unsolvable problem, you are given a computer program and a precise specification of what that program is supposed to do (e.g., sort a list of numbers). You need to verify that the program performs as specified (i.e., that it is correct). Because both the program and the specification are mathematically precise objects, you hope to automate the process of verification by feeding these objects into a suitably programmed computer. However, you will be disappointed. The general problem of software verification is not solvable by computer. - Sipser 2006 p. 201 I can see two strategies to prove this important theorem whose importance is increased when we think about its implications in proving artificial general intelligence (AGI) safety or value alignment. First,