More light-heartedly, for those who find this sort of thing fun, a while back I made a little puzzle (inspired by Bill Gosper) to illustrate the inherently deep difficulty of program verification: ======== A predicate on positive integers: boolean isToad(int n) { return ( n==2 || n==frog(4,floor((n-1)/2),1,0)-1) ); } is defined with the aid of the following helper method: int frog(int q, int r, int s, int t) { if (r<t) { return 0; } else if (r==t) { return 1; } else if (q==0) { return 0; } else { return ( frog(q,r,s+1,s+t) + frog(q-1,r-t,1,0) ); } } Questions: 1. Which integers are toads? 2. Can you describe what the frog method does? 3. Can you explain why this code works? ======== Without spoiling it: 1. Just run the program on successive n and it will quickly be obvious what "toads" are. Take this as the "requirements" or "specification" to be validated against. 2. Documenting what the frog code is computing is, in theory, only a little harder. But I've found programmers and their ilk often struggle mightily with this--until they abandon certain preconceptions about how it "ought" to be working. 3. Many funsters could answer this, but most software professionals boggle. I look forward to meeting the AI that can do it! "Enjoy"!