Newsgroups: comp.lang.misc Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!lavaca.uh.edu!menudo.uh.edu!sugar!ficc!peter From: peter@ficc.ferranti.com (Peter da Silva) Subject: Re: Formal definitions (Re: ada-c++ productivity) Message-ID: Reply-To: peter@ficc.ferranti.com (Peter da Silva) Organization: Xenix Support, FICC References: <1991Apr8.080931.23209@netcom.COM> <50097@nigel.ee.udel.edu> <50419@nigel.ee.udel.edu> Date: Fri, 12 Apr 91 16:40:43 GMT In article <50419@nigel.ee.udel.edu> new@ee.udel.edu (Darren New) writes: > In article peter@ficc.ferranti.com (Peter da Silva) writes: > >In article <50097@nigel.ee.udel.edu> new@ee.udel.edu (Darren New) writes: > >> You can also write programs which could not possibly be implemented in > >> C, even by Dan Bernstein :-). What more proof do you need? > >This is as insane a claim as any of Dan's. If it's implementable in > >principle it's implementable in C. It might take building another > >language on top of C to make it convenient, but it's implementable. > If you look closely at the complete post, you will notice that I never > claimed that all LOTOS programs are implementable. Well, you said there wasn't currently a compiler available for it. That doesn't say the same thing as "it's not implementable". > 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 ... [ formal specifications for SDI ] > >Is there an alternative? How do you specify hardware and human actions > >based on a formal language specification? > 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...)? > 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? -- Peter da Silva. `-_-' peter@ferranti.com +1 713 274 5180. 'U` "Have you hugged your wolf today?"