Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!usc!wuarchive!udel!ee.udel.edu From: new@ee.udel.edu (Darren New) Newsgroups: comp.lang.misc Subject: Re: Formal definitions (Re: ada-c++ productivity) Message-ID: <50097@nigel.ee.udel.edu> Date: 8 Apr 91 20:30:58 GMT References: <27FB56D8.6176@tct.com> <1991Apr8.080931.23209@netcom.COM> Sender: usenet@ee.udel.edu Organization: University of Delaware Lines: 159 Nntp-Posting-Host: snow-white.ee.udel.edu In article <1991Apr8.080931.23209@netcom.COM> mrs@netcom.COM (Morgan Schweers) writes: > 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? Maybe that it doesn't do the same thing on my configuration, or over my network, or with my version of the compiler as it does with yours. As an example, there are programs on the Amiga written before the formal method for determining PAL vs NTSC was decided. These usually didn't work when written in Europe and run in the USA. Ever get a C program that compiled when int==long but not when int==short? That was formally defined (in some sense) back in K&R. When people ignored that definition and played loose with what their compiler accepted, things break. > 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. No need to insult formal languages or their users just because they don't do what *you* want, especially when you later admit you have no clue what you are talking about. It's like saying "before you tell me that Ryder is better than U-Haul, understand that I drive race cars for a living." You can't draw conclusions on which truck is better for moving on such a basis. If you program where every cycle counts (and you should, if you are doing what I would call systems programming) then formal languages probably can't be compiled as efficiently as you want them to, because they either have to work the same independant of machine or there has to be decisions you make for your machine that you wouldn't otherwise need to make. However, most of us don't program where every cycle counts (especially when it's not worthwhile after you system programmer clowns destroy the efficiency with hack coding :-) and do program where continued correct execution is important. > 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. What do you mean by "bug-proof"? You mean a language where no programs have bugs, or a language where all bugs are caught? Normally, a formal language defines the exact effects of any syntactically valid program. Of course, if what you tell it to do is not what you want it to do, then you are not going to get what you want. > Show me one that is supposedly USEFUL, and I'll *WRITE* a bug in it! ;-) Take a look at LOTOS. It's completely mathematically defined. It's not even difficult to understand. It is very powerful, allowing definitions of any arbitrary data types that are no more infinite than integers. It also handles complex parallel evaluation. Is it useful? Very. Is it compilable? Not yet, that I know of. Then what good is it? I can describe TCP and IP completely and formally in about 5 pages. I can *communicate* to you exactly what you do in all cases, including reception of packets not to you, conflicting option bits, empty packets, all the errors which you would normally have missed because you didn't think about that case, etc, etc, etc. Also, I can *know* that all of that has been communicated and that I have not forgotten anything. This is an example of a very useful formal language (I can direct you to conferences which will attest to its usefulness) that you can't even compile. >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. LOTOS is quite a bit more flexible that any compilable language I've seen. At some point, you have to make your program work on more than one configuration. You also have to know that it meets the customer's specifications. How do you do that with C? With LOTOS, you can prove that your functionality is a superset of the customer's specification. You can also write programs which could not possibly be implemented in C, even by Dan Bernstein :-). What more proof do you need? > Also, to me, a formal specification consists of a grammar, and a >description of the basic keywords. Period. Then you have never seen a *real* formal specification and you shouldn't be claiming they are useless, since you've obviously never tried to use one. :-) >Don't give me math crap. I'm a programmer, not a math >junkie. I don't think you need to be a "math junkie" to understand LOTOS, but you can't have a formal definition without math. LOTOS's definition is really very simple. Much simpler than C. About as simple as FORTH or LISP. > *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. This leads me to believe you have no clue what you are talking about. *IF* your productivity ever depended on anybody else understanding what you are doing (like a project long enough that 80% of the people finishing it were not around when it was started and big enough that many people don't ever see other people working on the same program), then formal languages are a great bonus. A formal definition does not necessarily make a language any more restrictive than C is. From everything I know about Turing (not much :-), it is about as flexible as C and somewhat more powerful. >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!) This has nothing to do with formal definitions. Pascal has a formal definition, but certainly your friend isn't using it. (Pascal was not originally formally defined, but somewhere I have a reference for a formal definition thereof.) > 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'. I suspect you have the wrong idea what "safe" means. Formal means that every sequence of operations you perform either has a defined result or you know it doesn't. For example, in C, running off the end of a malloc'ed array isn't formally defined. "Faithful" means that it either does what is defined or the run-time system tells you about it. For example, if array bounds are checked, then array bounds are "faithful." If everything is faithful, then referencing disposed memory is caught, uninitialized variables are caught, and so on. I'm not sure what you mean by "safe." >The two are incompatible, in my (admittedly limited) >experience. Prove me wrong. Feel free. Check out LOTOS. Then talk to anybody who designed a 50,000 line network protocol product after specifying it in LOTOS. Talk to the people they hired halfway through the development and ask them how long it took them to get up to speed (probably about a week). Talk to the customers, who had a contract based on a formal definition of the desired service, and how they could 1) settle whether there was a bug or not, 2) could get realistic estimates on construction and modification times/costs, etc etc etc. How do you know Ada's validation suite tests all the semantics of Ada? Do you want to build SDI based on "I think so"? >+--------------- > My company wouldn't really understand this discussion, so I can't imagine >what their opinions would be. -- mrs@netcom.com >---------------+ Actually, I bet *somebody* there *would* understand this discussion (given a name like "netcom", if that really is where you work). Ask around, and see if you can find somebody who understands LOTOS or Estelle or SDL. Networking is really where formal techniques are best applied, because it tremendously aids in human-to-human communication as well as human- to-machine. -- Darren -- --- Darren New --- Grad Student --- CIS --- Univ. of Delaware --- ----- Network Protocols, Graphics, Programming Languages, FDTs ----- +=+=+ My time is very valuable, but unfortunately only to me +=+=+ + When you drive screws with a hammer, screwdrivers are unrecognisable +