Steven D'Aprano <steve+comp.lang.pyt...@pearwood.info> writes:
> On Mon, 19 Feb 2018 09:40:09 +0100, Alain Ketterlin wrote:
>
>> Tim Delaney <timothy.c.dela...@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.
--
https://mail.python.org/mailman/listinfo/python-list
