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

[Steven D'Aprano]

On Mon, 19 Feb 2018 12:19:14 +0100, Alain Ketterlin wrote:

> 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).

I didn't ask about theorem provers. I asked about type systems.

https://en.wikipedia.org/wiki/Automated_theorem_prover

One could, in principle, add a theorem prover to a type system, or at 
least add certain theorem-proving-like functionality to it, but at what 
point does the type checker become complex enough that we can no longer 
trust it? If you don't understand the proof that code is bug-free, you're 
really trusting that the type-checker is bug-free.


> Here is one that makes your point much better:
> 
>     if a**n + b**n == c**n:
>         print("hello world")
>     else:
>         fire_missiles()

Either way, I doubt any existing type systems could eliminate the dead 
code in those examples. If you know of one which would, I'd be interested 
to hear about it.


>> 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.

That's not what I am saying. You're putting words into my mouth and 
criticising me for a position much more extreme than I've expressed.

If you search the archives to this list, you'll see that I've frequently 
supported Python adding type-hints to the language[1], to allow tools 
like MyPy and various linters to perform static analysis on Python code. 
Especially for large projects, that can be helpful.

Type-checking is yet another tool for gathering evidence (not "proving") 
that a program is correct, together with (among others) code review and 
especially testing.

As Donald Knuth said:

"Beware of bugs in the above code; I have only proved it correct, not 
tried it."

What I object to is the idea that static type-checking is "indispensable" 
or sufficient. Its one tool out of many, and more dispensable than some 
of the others.

Even in a big project, which would you rather give up: all testing, or 
all static type checking?

I don't just mean all formal tests, but even running the code to see if 
it works. Literally "it compiles, ship it!". No, I don't think so.

Testing is truly indispensable, whether they are formal tests or not. 
Static typing and "type-safety", not so much.





[1] If you search far back enough, you may find me taking a more extreme 
position that static typing was unnecessary. That was a much younger and 
more naive me.



-- 
Steve