Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!swrinde!elroy.jpl.nasa.gov!ames!vsi1!daver!dlb!netcom!mrs From: mrs@netcom.COM (Morgan Schweers) Newsgroups: comp.lang.misc Subject: Re: Formal definitions (Re: ada-c++ productivity) Message-ID: <1991Apr8.080931.23209@netcom.COM> Date: 8 Apr 91 08:09:31 GMT References: <4ebGltlf1@cs.psu.edu> <27FB56D8.6176@tct.com> Organization: McAfee Associates Lines: 96 In article schwartz@groucho.cs.psu.edu (Scott Schwartz) writes: > >According to Chip Salzenberg: >| According to Scott Schwartz: >| >How do you know that the validation suit tests for the language that >| >ANSI specified? >| >| I don't. I suppose that should worry me. *yawn* > >It worries me. It also worries me that you aren't worried. > This is because you see everything in terms of 'theory' and not 'practice'. (Inferred from your various comments.) I'm not a theory person either, so it doesn't really worry me either. The point is that if I can get somethine to *WORK* then to hell with all the theory in the world. 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? >| >Some languages, like Turing, were formally specified from the time >| >of inception; you can run a program and mechanically decide if it >| >did what the language definition said it should do. Yes, but can you get any *WORK* done in it in a reasonable amount of time? How powerful is it? How can you tell the difference between a program that is 'decided to be incorrect' and an OS which forces an error condition on the program? Does it *REALLY* matter? You can build your theoretical languages all you want, but if they don't add to my ability to produce smooth, working code, I'M NOT GOING TO TOUCH THEM! I'm a systems programmer, so decide before you respond, if your language (probably supposedly universal across all implementations, if I know you theory weenies) will do the job for what I consider real work. >| >| How do you know that the program that makes that decision doesn't have >| a bug in it? > >It might, but that's just one program, not 50 different compilers with >5,000 test cases. It's easier to feel sure about. Consider this... > >* Because the language was unambiguously specified I have more >confidence in the people writing the software. For one thing, if you >know what the mission is in advance, it is that much easier to >accomplish it. For another, having a mechanically interpretable >formal specification means you can build software tools to help the >entire process along, just as having a yacc grammer for some language >makes it easier and more reliable to write a parser. There may be >bugs, but debugging small well specified tools is easier and more >effective than debugging large ill-specified final products. > >* If a formal description of a programming language is available >it makes it _possible_ to decide the question you ask. Absent such a >description the best you can do is flame about it on usenet for a few >weeks. Get serious. If you come up with a language that is guaranteed to be bug- proof, I'll show you a language with a BEGIN and an END which can be inter- changed, and NOTHING ELSE. Show me one that is supposedly USEFUL, and I'll *WRITE* a bug in it! ;-) > >| At some point, you have to stop assuring and start doing. > >Sure. That's the argument in favor of dynamic typing that has been so >well received here recently. What I'm suggesting is that providing a >formal specification of a language is the software engineering analog >of using things like parser generators and static type checking. Yes, >no system is perfect, but gee, why make it harder on everyone? YOU are the one looking to make things harder. Software Engineering? Get real. Perhaps it's the bad associations I've had with people calling themselves Software Engineers (they worked in Ada, Modula-2 and COBOL), but Software Engineering For Better Programs is nonsense. If you have a language that makes it possible to 'prove' the program correct, then you have a language which is probably putting too many restrictions on the programmer. 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. *IF* you can make me more productive, I'd look at what you were talking about. The important point here is that *I KNOW WHAT I'M DOING* and I don't want a language that told me I didn't. I could program in Pascal or some other psuedo-useless language if I wanted that. (I have a friend who is forced to program in Pascal. You should hear him scream for type-casting!) The point is that there are tradeoffs involved, and that there is *NO WAY* you are going to design a language that will be both completely useful and completely 'safe'. The two are incompatible, in my (admittedly limited) experience. Prove me wrong. Feel free. -- Morgan Schweers +--------------- My company wouldn't really understand this discussion, so I can't imagine what their opinions would be. -- mrs@netcom.com ---------------+