python philosophical question - strong vs duck typing
edriscoll at wisc.edu
Wed Jan 4 11:15:03 EST 2012
On 1/4/2012 12:37 AM, Terry Reedy wrote:
> Using induction, I can prove, for instance, that these two functions
> 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.
More information about the Python-list