From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 109fba,b87849933931bc93 X-Google-Attributes: gid109fba,public X-Google-Thread: fac41,b87849933931bc93 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,b87849933931bc93 X-Google-Attributes: gid103376,public X-Google-Thread: 114809,b87849933931bc93 X-Google-Attributes: gid114809,public X-Google-Thread: 1108a1,b87849933931bc93 X-Google-Attributes: gid1108a1,public From: dewar@merv.cs.nyu.edu (Robert Dewar) Subject: Re: OO, C++, and something much better! Date: 1997/01/29 Message-ID: #1/1 X-Deja-AN: 213032827 references: <6PI998tV3RB@herold.franken.de> <5c4ab5$134$1@goanna.cs.rmit.EDU.AU> organization: New York University newsgroups: comp.object,comp.lang.c++,comp.lang.ada,comp.lang.smalltalk,comp.lang.eiffel Date: 1997-01-29T00:00:00+00:00 List-Id: Bob Duff said "But, to be fair, to the dynamic-typing folks, static checking can't prove the absense of bugs, either. There is no silver bullet. Static checking eliminates *some* bugs, and that's good. A catch-phrase like "testing can't eliminate bugs" isn't helpful, since no other technique is perfect, either." Well that's a little misleading. Static checking does indeed prove the absence of certain kinds of bugs. How far you want to expand this set of errors that can be eliminated completely and reliably is one of the fundamental design parameters in design of PL's. YOu can indeed go very far. Look for instance at the programming language that is derived from Martin Lof logic. In this language, it is impossible to write any program that is not totally correct in a formal sense. Of course the program might not do what you want (Bob's comment about the correctness of the specs themselves is of course a fundamental one), but you can't get any type errors, interpreted in the broadest possible sense, and the prrogram is guaranteed to terminate with an output that conforms to the specification. The trouble with going in this direction is that you do limit expressive power. Martin Lof logic for example allows only primitive recursion as a control construct (*), and also you arrive at a formalism that is proably beyond the capabilities of most programmers. P.S. (*) primitive recursion is a little more powerful than people suppose, there is for example no problem in programming Ackerman's function using primitive recursion with higher order functions. P.P.S. Is there a separate newsgroup which would be more appropriate to these general programming language discussions. It seems to me that these heavily cross-posted discussions probably constitute serious and annoying noise for the majority of readers of all groups concerned.