🚀 go-pugleaf

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 +