Are the critiques in "All the things I hate about Python" valid?

[Alain Ketterlin]

Steven D'Aprano <steve+comp.lang.python at pearwood.info> writes:

> On Mon, 19 Feb 2018 09:40:09 +0100, Alain Ketterlin wrote:
>
>> Tim Delaney <timothy.c.delaney at gmail.com> writes:
>> 
>> [...]
>>> As others have said, typing is about how the underlying memory is
>>> treated.
>> 
>> No. It is much more than that. Typing is about everything you can say
>> about a given statement.
>
> "Everything"? Truly *everything*?

Everything you can say.

> Given:
>
>     # engage the type system somehow...
>     # declare a, b, c: non-negative integers
>     a = abs(int(input("Give me an integer")))
>     b = a*a
>     c = (a+1)*(a+1)
>
> can you give me an example of a type-system which is capable of telling 
> me that:
>
>     if (c - b) % 2 == 1:
>         print("hello world")
>     else:
>         fire_missiles()
>
> will never fire the missiles?

Your example is ridiculously simple for all theorem provers I know (not
on Python code of course, since you can't even be sure int() etc. have
not been redefined).

Here is one that makes your point much better:

    if a**n + b**n == c**n:
        print("hello world")
    else:
        fire_missiles()

> I'd be impressed enough with a type system that knew that a%2 was always 
> 0 or 1, although I suppose there could be some that already know that.
>
> Hell, I'd even be impressed if it could tell that c was not zero...

Your claim essentially is: since we cannot prove everything, let's not
even try to prove anything. Go on if you think this is the right way to
think about typing.

-- Alain.