On 1/4/2012 12:37 AM, Terry Reedy wrote: > > Using induction, I can prove, for instance, that these two functions > [snip] > are equivalent, assuming enough stack and normal procedural Python > semantics. (And assuming no typos ;-).
YOU proved that; your type system didn't. With a powerful enough type system, those two functions would have the same type, while if you had made a typo they wouldn't. The extreme example of a powerful type system is something like Coq or Elf. In a language like that, a mathematical sentence is encoded in a type, and "objects" of a certain type represent a proof that that the sentence can be proved. Evan -- http://mail.python.org/mailman/listinfo/python-list
