Who is the world's oldest working programmer?

When mathematicians can't prove something, they try and transform it to something they can prove. So rather than prove the correctness of the original program, use tools to re-structure and re-write the program in such a way that the difficulties are eliminated. For example look at the techniques used to unravel the wonderful obfuscated 12 days of Christmas.... http://research.microsoft.com/en-us/um/people/tball/papers/xmasgift/ I am pretty sure tools be developed to take a program with the issues you mention and from it produce a functionally equivalent program, whose correctness would be more easily provable.. Indeed, as how do you specify the functional requirements of a program in way such that there are no ambiguities in the specification? Well perhaps you write pseudo code and I suggest that if you write pseudo code, then can I suggest it would be possible to produce algorithms for converting the pseudo code to most any language in such a way that the converted code will be provably correct.... Trying to prove an arbitrary program implements a specific function is challenging.... Dave G4UGM