🚀 go-pugleaf

RetroBBS NetNews Server

Inspired by RockSolid Light RIP Retro Guy

Article View: comp.lang.misc
Article #3405

Re: Formal definitions (Re: ada-c++ productivity)

#3405
From: Morgan Schweers
Date: Mon, 08 Apr 1991 08:09
96 lines
5699 bytes
In article <p79Gyx1j1@cs.psu.edu> 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
---------------+
Technical Details
Message-ID: <1991Apr8.080931.23209@netcom.COM>
Path: arc1-ca.pugleaf.net!utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!swrinde!elroy.jpl.nasa.gov!ames!vsi1!daver!dlb!netcom!mrs
References: <4ebGltlf1@cs.psu.edu> <27FB56D8.6176@tct.com> <p79Gyx1j1@cs.psu.edu>

Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!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> <p79Gyx1j1@cs.psu.edu>
Organization: McAfee Associates
Lines: 96