🚀 go-pugleaf

In article <MBOA8C9@xds13.ferranti.com> peter@ficc.ferranti.com (Peter da Silva) writes:
>In article <50419@nigel.ee.udel.edu> new@ee.udel.edu (Darren New) writes:

>Well, you said there wasn't currently a compiler available for it. That
>doesn't say the same thing as "it's not implementable".

I said "Can you compile it?  No."  if you want to be picky :-)

>> Of course, programs which you write based on a LOTOS
>> specification will not necessarily implement the full specification,
>... and may be written in C as well as anything ...

No argument. Of course, if you *do* write it in LOTOS (the subset that
you could compile) then you can be sure it implements what was
specified.

>> I understand a CPU called "viper" has in some way been formally validated.
>Fine. How about the rest of the system (up to and including launch vehicles,
>ordnance, sensors, etc...)?

Probably not.  What's your point?  I'm not trying to say that formal
specifications can prevent you from needing to test anything.  I'm
merely saying that they *help*.  Tastes great, less filling.

>> Also, law-goverend systems
>> can formally specify the ways in which people are allowed to interact
>> with the system, including the ways in which they are allowed to change
>> the code and the laws themselves.

>I see, the formal specification rules out infiltrating the U.S. with small
>nuclear devices hidden in Ford Econoline vans?

Well, the quality of this post is certainly not up to the standards I've
come to expect from your posts.  If you forgot the :-)'s then I understand.

I can't imagine what blowing up the computer has to do with whether
there are bugs in a program due to misunderstanding of what the
compiler is supposed to support.  It's also possible to have the police
arrest and beat to death the programmers; does that mean we shouldn't
have laws?

Sorry for mentioning these other formal systems.  It was my impression
that you might be interested in hearing about something you might not
know about, rather than pointless flamage.   Geez.    

>Peter da Silva.  `-_-'  peter@ferranti.com

	 -- 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 +=+=+