Article View: comp.lang.misc
Article #3459Re: Formal definitions (Re: ada-c++ productivity)
From: Morgan Schweers
Date: Fri, 12 Apr 1991 06:49
Date: Fri, 12 Apr 1991 06:49
191 lines
10333 bytes
10333 bytes
Some time ago schwartz@groucho.cs.psu.edu (Scott Schwartz) happily mumbled:
>
>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.
Yes, I was ranting. I *hope* I didn't use the phrase 'theory weenie
in my text, though I admit that I was thinking it. <Grin> Perhaps I
underused (can you say, none-at-all?) smileys, or some-such. I really
did mean most of what I said, but I didn't mean it as a flame.
Tangible benefits from precision, eh? I tend to see people putting
too much emphasis on 'precision' and not enough on, 'does it work?'
>
>| 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.
I recently had a chance to observe JUST THIS SYMPTOM. The Microsoft
C(6.0) compiler has an optimization bug that broke my code. The program
got tested (I don't *LIKE* the way it was tested, but that's my boss's
decision) and we found that it failed under certain circumstances. I
fixed the problem (fixed the optimization) and went on with life.
Is this a compiler bug? Of certainty! Is this something which would
make me consider changing languages? Certainly not! Would it even make
me consider changing compilers? It's not in my hands to do that. Would
I have the same problem under other optimizers? Maybe, maybe not. Would
I have the same problem under LOTOS, if it were compilable? Maybe, maybe
not. You can brag about 'bug-checking' in the source files all you want,
but the executables are where it matters.
If your optimizer has the same 'features' as the Microsoft C compiler,
then it'll still break my code. It's the object code that does the work,
and that's where everything matters. You can 'formalize' all you want,
but the end result is whatever the compiler does.
>
>| Yes, but can you get any *WORK* done in it in a reasonable amount of time?
>
>I type "make". How do you do it?
This is a statement just BEGGING for a flame...
#ifdef FLAME
Really? 'make' writes all your code for you, automatically choosing
the correct language, for the problem that you've envisioned in your
mind? It then proceeds to 'prove' the programs correctness within
the parameters not supplied to it? It then does beta-testing on the
program, as well as speed and accuracy tests?
D'you mind if I borrow your 'make' program, I'd *REALLY* like a
copy of it. As I said, if it'll improve my productivity, no
problem!
Goddamn dweeb. (Note: Obligitory flaming ad hominem attack.)
#endif
>
>| 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?
Ah, but this wasn't the original point. The original point was a
person (yourself?) discussing the advantages of a language in which it
could (supposedly) be proven that a program would work as designed.
If the ANSI committee stripped C of it's functionality in the
process of making it 'formalized' I'd simply not use an ANSI compiling
C compiler.
Standards exist to make things work between different platforms. I
understand that this statement is going to be met with *FLAMES*, BUT
the following holds true for my particular field. IF you are doing
bit level systems programming, your code ain't likely to be very
portable. It's also *NECESSARY* to be fast, and compact.
I understand the need for portable programming. It's a great thing,
and I've made excellent use of it in the past (porting my favorite
utilities to various platforms.) However, no language (IMHO) can be
fully formalized and be fully useful on all platforms. The fact is that
each individual platform has certain features that you can take advantage
of that will boost your productivity and your codes power.
Yes, you should create a seperate module for system specific stuff,
*BUT* the point is that the language has to allow it. If a language is
fully formalized (in the manner I've noted) then it's not likely (note,
I said not *LIKELY*) to be able to encompass new features on new hardware.
If it can't allow for system specific modules, then it's going to be
a rapidly dead language. If it does allow for system specific modules,
it's got to understand that it's going to be different from system to
system. And after all, how *DO* you formalize what the input value from
port 70h is?
>
>| 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?
Yes, I realize that a BNF grammar <etc>, but I also *feel* that
the grammar of a language should be variable by implementation. With
a fully 'formalized' language, this isn't (to the best of my knowledge)
true. It's also worth noting that you *did* mention a compiler
IMPLEMENTOR making these choices. That's up to the implementor, and
I'll live with their changes. What you (or whomever) was advocating
was that it be in the formal spec. I also hold the opinion that the
programmer should be able to override the above-mentioned options and
make them either warnings, or totally ignored. If not that, then
give me an implementation where it is possible to get AROUND those
limitations.
>
>| *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.
<Grin> Thanks. I've got some CaffieneCola in front of me, and
a bag of chips. I'm feelin' fine... I don't watch TV, but I do have
Kraftwerk blaring in my ears. I understand your meaning, but *DESPITE*
the sound of my article, I really don't mean to flame.
In re: lint... Some compilers don't come with 'lint' because they
chop the programmer's head off in the name of 'pretty programming'.
I like 'lint' and similar programs, because I can feel free to ignore
their results. The languages which *don't* include them tend to FORCE
me to follow their idea of good programming.
This entire bag of...chips...is really a religious war, in
disguise. (A *THIN* disguise.) I wasn't really aware of that
when I posted my message, but I am now. <Sigh> My entire set of
experiences with programming has been mainly to get the most
ability out of the equipment I'm on. I often resort to assembly
language to do it, so I have a certain callous attitude towards
the idea that a language with a lot of constraints can fix the
worlds problems. To bastardize HEAVILY a standard quote,
"When the main tool one has used is a swiss-army knife, one tends to
look down on people who claim that a single screwdriver could do it
better."
I've used Lisp, Snobol, Fortran and many other languages that
constrain me. I'm very guilty of using the best tool for the job,
I suppose. It's an unforgivable trait, I've noticed. However, the
*IDEA* of programming in a language that was *DESIGNED* to constrain
the programmer is insane. (Note, I've also used Pascal, but not for
anything serious, thank you.)
This is a *HELL* of a lot longer than I had intended it to be, but
here it is. Flamage is in the eye of the beholder. I admit, now, to
being a poor speller, a poor writer, and any other grammar flames you
might have. I also admit to being a short-sighted, ignorant, clueless
programmer if it'll make you feel better. (*I* don't have to believe
it, but if it'll shut the people who are likely to flame me up, I
don't care.)
OBTW, if my facts are out of order feel free to correct me. I
read this group often, and am always willing to learn. (Despite
whatever you may think of my postings.)
-- Morgan Schweers
+--
The people at my place of employment wouldn't understand this
discussion, except for one. He's the other programmer. He's not
around, so I can't ask his opinion. So there. -- mrs@netcom.com
--+
Technical Details
Message-ID:
<1991Apr12.064938.5274@netcom.COM>Path:
arc1-ca.pugleaf.net!utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!mips!pacbell.com!tandem!netcom!mrsReferences:
<p79Gyx1j1@cs.psu.edu> <1991Apr8.080931.23209@netcom.COM> <+xcGphhk1@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!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.064938.5274@netcom.COM> Date: 12 Apr 91 06:49:38 GMT References: <p79Gyx1j1@cs.psu.edu> <1991Apr8.080931.23209@netcom.COM> <+xcGphhk1@cs.psu.edu> Organization: McAfee Associates Lines: 191