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

[Steven D'Aprano]

On Sun, 18 Feb 2018 19:38:03 -0500, Dennis Lee Bieber wrote:

> On Mon, 19 Feb 2018 00:09:40 +0000 (UTC), Steven D'Aprano
> <steve+comp.lang.python at pearwood.info> declaimed the following:
> 
> 
>>Or more realistically, suppose you want your type system to ensure that
>>you don't lay off the wrong workers:
>>
>>"employee records where the length of employment is greater than six
>>months but less than five years, AND the salary is greater than $100,000
>>or less than $40,000, AND the average number of paid sick days taken per
>>year over the last three years is less than five, AND the number of
>>reprimands is zero in the last year and less than two in the last five
>>years, AND the position in the last two stack rankings was in the top
>>fifty percent"
>>
> 	That's not a data type -- that's an SQL query...
> 
> 	The data type is still "employee"


Dennis, you've missed the context.

We're discussing the claim that given a sufficiently fine-grained type-
system, type checkers can prove any program is correct. Under that 
scenario, we need separate types for integers, positive integers, 
negative-or-positive-integers-but-not-zero, employees, employees with 
seniority, employees with reprimands on their file, employees with three 
or more reprimands on their file, etc.

Every tiny distinction between data values becomes a type, and (so the 
claim goes) the type checker can prove that your program is 100% bug 
free. You will never accidentally fire the wrong person, because the 
compiler won't let you call file_employee(x) if x is the wrong type of 
employee.

Of course its nonsense, but that's the claim I'm discussing.


-- 
Steve