Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!mips!pacbell.com!tandem!netcom!mrs From: mrs@netcom.COM (Morgan Schweers) Newsgroups: comp.lang.misc Subject: Re: Formal definitions (Re: ada-c++ productivity) Message-ID: <1991Apr12.082128.11654@netcom.COM> Date: 12 Apr 91 08:21:28 GMT References: <1991Apr8.080931.23209@netcom.COM> <50097@nigel.ee.udel.edu> Organization: McAfee Associates Lines: 170 Some time ago new@ee.udel.edu (Darren New) happily mumbled: >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? > [Very good arguments about playing 'fast and loose'] > I agree. However, there are (IMO) circumstances in which you *MUST* have the capability to play 'fast and loose.' If you think this isn't true, then your just not doing the same jobs as I am. >> 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. > You're right. No argument. *IF* however, someone claims that I should drive a truck on the racetrack because it's got a better safety record than my racecar, I'll laugh in their face. I think you would too, in the same circumstances. > 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. Hack coding improves the efficiency. I never claimed that it was PRETTY, but it improves the efficiency. If it didn't, it wouldn't be hack coding. ;-) > >> 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. And if the input is undefined, and you have to adjust to circumstances? What if you're writing a neural network program. Will the 'formal language' tell you all possible exact effects? How about an OCR program? I call bullshit on that. For a limited set of inputs, in a controlled environment, it's possible. For real-world problems and real-world systems, I say it's not possible. See my other responses for why. > >> 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? Really? It's not compilable, eh? Sounds real similar to BNF to me. I accept that these are useful. You can't *PROGRAM* in them, but they are useful as references. The point is that you have to write it in a compilable language at some point. Your original can be a flowchart, a BNF, a LOTOS program, or scribblings on a piece of toilet paper, but your code has to go through a real compiler. That's where the work gets done. By the programmer who does the implementation. He can't be programming in a language that doesn't run, for obvious reasons. He can define the algorithms however he wants, as long as the result is what comes off the spec. I understand this, as does (I would imagine) all other programmers doing Real Work(tm). It's the concept that I should program in a 'formalized' language that makes me laugh. It's the idea that I should be worried that the language ISN'T formally provable that makes me laugh. > >>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 ^^^^^^^^^^^^^^^^^^^^^^^^^^ (You test it.) >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? Who *IS* this Dan Bernstein guy? You're the second person to mention him. Yeah, 'more flexible than any compilable language', etc. Sheesh. Do you ever get any work done? You write the specs for the customer, no problem. I'll take it and make it work. Right? Right. > >> 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. :-) So enlighten me, mortal. > >>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 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ (Why?) >is really very simple. Much simpler than C. About as simple as FORTH >or LISP. > > [Good stuff about big projects, and such.] You're right, to an extent. However, some projects are never 'finished' and cannot have a formal spec at the beginning because it *MUST* change by the end, and would hamper more than help. You've probably never wortked on a project like that, so we really are talking from two different points of view. > [More good points about 'faithful' as a concept.] Too true. I meant 'safe' as 'faithful' I suppose. Consider that much of the code involved in the sort of work that I (and many other programmers) do would fall under the heading of 'undefined' results. (More specifically, platform-defined, or situation-defined.) If the sole purpose for the language is to have a language whose results can be checked, as long as they are defined, then it makes no sense to use it for things that will normally be site-defined. Does that make sense? Why use an innappropriate tool? > >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"? > For the Real Time mode of something like SDI, I wouldn't trust Ada as far as I could throw Congress. You're talking about 'Catastrophic Failure' if speed-deadlines aren't met. Catastrophic failure in a Big Way! ( ;-) ) Netcom is a service from which people 'lease' accounts. Network Communications, obviously. It's a service. My company is a small software firm, so some of your comments don't apply. Of course, SINCE it's a small company, I'm sure many of my comments don't apply to you, wherever you work. >--- 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 + -- Morgan Schweers P.S. This has gotten *WAY* out of hand. We're talking about messages 200+ lines in length, constantly. I love the discussion, and am waiting for someone to define Formal Languages, but it's getting a bit long. Will anyone settle for a pathetic, "We have different opinions, because we do different jobs?" or is this determined to be a continuing thread? +-- "When you've used a swiss-army-knife for years, it's hard to imagine working with only a spoon." -- mrs@netcom.com --+