Newsgroups: comp.lang.misc Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!wuarchive!psuvax1!news From: schwartz@groucho.cs.psu.edu (Scott Schwartz) Subject: Re: Formal definitions (Re: ada-c++ productivity) In-Reply-To: mrs@netcom.COM's message of Mon, 8 Apr 1991 08:09:31 GMT Message-ID: <+xcGphhk1@cs.psu.edu> Sender: news@cs.psu.edu (Usenet) Nntp-Posting-Host: groucho.cs.psu.edu Organization: PSU CS References: <4ebGltlf1@cs.psu.edu> <27FB56D8.6176@tct.com> <1991Apr8.080931.23209@netcom.COM> Date: Mon, 8 Apr 91 21:22:10 GMT Lines: 61 Morgan Schweers rants: | This is because you see everything in terms of 'theory' and not | 'practice'. Not a bit. I'm not a "theory weenie". On the other hand, part of the fun of writing programs is that you get tangible benefits from precision. | I don't need a language to be formally accepted, or formally tested, | to write code in it. I do the testing on my program. If the | compiler breaks it, I'll worry about it. If the compiler doesn't | break my code, whassamatter with it? How can you tell if it is a compiler bug, or a bug in your code, or a bug in your understanding? Someone has to specify what the langauge is supposed to do. It seems to me that if you can build software tools to help implement the language you will get a better result. | Yes, but can you get any *WORK* done in it in a reasonable amount of time? I type "make". How do you do it? | How powerful is it? A flip answer is, "More powerful than what you are using now". A serious answer notes that your question has nothing to do with whether or not the language is formally defined. Suppose someone writes denotational semantics for C, and the ANSI committee stamps it with their seal of approval. Will you suddenly decide you hate C? | Also, to me, a formal specification consists of a grammar, and a | description of the basic keywords. Period. At that point, the language is | defined in terms of what I can use it for. What do you mean by a 'formal | specification'? Don't give me math crap. I'm a programmer, not a math | junkie. Great... just when hostile usenet junkies get tired of accusing Dan Bernstein of being a computer scientist, they start accusing me of being a mathematician. You realize that a BNF grammer is a formal specification of syntax, right? (Or are you opposed to parser generators too?) What objection do you have to an analagous formal description of semantics? Why shouldn't the C compiler implementor be able to directly code the fact that type widening is unsigned preserving (or is it value preserving?), or that you are allowed to index but not dereference one element past the end of an array? | *IF* you can make me more productive, I'd look at what you were | talking about. The first step is for you to sit down and drink some orange juice and watch some tv. Don't read usenet until you feel better. :-) Next time you run "lint" think about the kinds of things it is checking. Then think about why not all compilers come with things like lint. Then think about why.