On Mon, 19 Feb 2018 12:19:14 +0100, Alain Ketterlin wrote: > 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).
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, 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.  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 -- https://mail.python.org/mailman/listinfo/python-list