Position statement: Can testing prove software has no bug?

The author presents a theorem that states that the correctness of a software system can be validated by testing on a finite number of test cases provided that the program and specification are in a learnable set of functions. Moreover, such testing can be performed without writing down a formal specification. This lays a foundation of the current practice of software testing where formal specifications are not available. This theorem implies that what current testing practice lacks is an analysis of the "complexity" of the program to determine a learnable set within which the program and the specification vary.