From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,93a8020cc980d113 X-Google-Attributes: gid103376,public X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news2.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!nx02.iad01.newshosting.com!newshosting.com!198.186.194.251.MISMATCH!news-out.readnews.com!transit4.readnews.com!panix!newsfeed-00.mathworks.com!nntp.TheWorld.com!not-for-mail From: Robert A Duff Newsgroups: comp.lang.ada Subject: Re: What is wrong with Ada? Date: Sat, 14 Apr 2007 18:47:10 -0400 Organization: The World Public Access UNIX, Brookline, MA Message-ID: References: <1176150704.130880.248080@l77g2000hsb.googlegroups.com> <461B52A6.20102@obry.net> <461BA892.3090002@obry.net> <82dgve.spf.ln@hunter.axlog.fr> <1176226291.589741.257600@q75g2000hsh.googlegroups.com> <4eaive.6p9.ln@hunter.axlog.fr> <1176454559.901200.34300@y80g2000hsf.googlegroups.com> NNTP-Posting-Host: shell01.theworld.com Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: pcls6.std.com 1176590830 15284 192.74.137.71 (14 Apr 2007 22:47:10 GMT) X-Complaints-To: abuse@TheWorld.com NNTP-Posting-Date: Sat, 14 Apr 2007 22:47:10 +0000 (UTC) User-Agent: Gnus/5.1008 (Gnus v5.10.8) Emacs/21.3 (irix) Cancel-Lock: sha1:ud8uOBjwhFaD59Had2bssEEqSW0= Xref: g2news1.google.com comp.lang.ada:15026 Date: 2007-04-14T18:47:10-04:00 List-Id: "Harald Korneliussen" writes: > On Apr 12, 8:47 pm, Robert A Duff > wrote: >> There is no way to be sure the code is bug free! Not in any language. >> Not using testing, nor any other method (including so-called >> proof of correctness). >> > In so-called dependently-typed languages, you can use the type system > to ensure the correctness of a program, ... OK, but if "correct" means "obeys a formal specification", then correct programs can have bugs. By "bug", I mean that reasonable users would consider it wrong behavior. In many cases, it's not even possible to formally specify what's "right" or "wrong" behavior. Proof: we've all witnessed arguments where one person says "it's a bug", and the other says "no, it's a feature". ;-) >...at least such a program as > your primality checker. The type-theorists talk about this curry- > howard isomorphism thing, which apparently is an isomorphism between > programs and proof. > > I think the SPARK people would agree that there are indeed methods to > assure that code is bug-free, at least to the extent that the > specification is bug-free... There's the rub. I've read studies that claim about half of all bugs are bugs in the specification. And of course many programs have no specification other than the program itself. Note also that SPARK is a very simple language, intended for very simple applications (i.e. safety is more important than fancy features). If you try to write, say, a windows operating system, or an Ada compiler, in SPARK, I think you would have trouble. That's fine -- it's not what SPARK is for. >... (and even that can to some degree be checked > mechanically!). Not to say that it is easy, cheap, or even feasible in > very many cases, but don't you underestimate a good type system. Agreed. SofCheck is makes a tool that can go far in this direction, in a practical way. But it's a dangerous mistake to think that some method or other can completely eliminate bugs. - Bob