python philosophical question - strong vs duck typing

[Evan Driscoll]

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