Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!rice!uupsi!ficc!peter From: peter@ficc.ferranti.com (Peter da Silva) Newsgroups: comp.lang.misc Subject: Re: Formal definitions (Re: ada-c++ productivity) Message-ID: Date: 15 Apr 91 14:56:26 GMT References: <50419@nigel.ee.udel.edu> <50577@nigel.ee.udel.edu> Reply-To: peter@ficc.ferranti.com (Peter da Silva) Organization: Xenix Support, FICC Lines: 37 In article <50577@nigel.ee.udel.edu> new@ee.udel.edu (Darren New) writes: > 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. OK, fine. You can implement a subset of LOTOS, and anything implementable in that subset is implementable in C. End of argument. > >> 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? That bringing up the SDI bugaboo is pretty much an irrelevant digression. Is viper fast enough to do the job? Will it remain so? > 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'm running out of smileys. I don't find SDI amusing. "Nuclear War can ruin your whole compile" -- Karl Lehenbauer. > 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. The symptom of a failure in SDI is nuclear explosions in major cities, remember. Hey, you brought up SDI. If you want to use a reasonable example against informal programming methods, or whatever, how about the Therac incident? Much more appropriate. -- Peter da Silva. `-_-' peter@ferranti.com +1 713 274 5180. 'U` "Have you hugged your wolf today?"