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,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,5bc4be576204aa20 X-Google-Thread: 101deb,cd56ecd4470caa13,start X-Google-Attributes: gid103376,gid101deb,public X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news4.google.com!newshub.sdsu.edu!logbridge.uoregon.edu!newsfeeds.ihug.co.nz!ihug.co.nz!ken-transit.news.telstra.net!ken-in.news.telstra.net!news.telstra.net!news-server.bigpond.net.au!53ab2750!not-for-mail From: "robin" Newsgroups: comp.lang.ada,comp.lang.pl1 References: <43783810.6080808@obry.net> <0f4ef.1413$s14.1261@newsread2.news.pas.earthlink.net> Subject: Re: Buffer overflow Article - CACM X-Newsreader: Microsoft Outlook Express 4.72.3110.5 X-MimeOLE: Produced By Microsoft MimeOLE V4.72.3110.3 Message-ID: Date: Wed, 30 Nov 2005 15:27:24 GMT NNTP-Posting-Host: 203.54.188.26 X-Complaints-To: abuse@bigpond.net.au X-Trace: news-server.bigpond.net.au 1133364444 203.54.188.26 (Thu, 01 Dec 2005 02:27:24 EST) NNTP-Posting-Date: Thu, 01 Dec 2005 02:27:24 EST Organization: BigPond Internet Services Xref: g2news1.google.com comp.lang.ada:6682 comp.lang.pl1:1401 Date: 2005-11-30T15:27:24+00:00 List-Id: Christopher Browne wrote in message ... >Something that is only approximately correct but that is super-fast >may, in cases where time or computational effort *are* at a premium, >be preferable to a slower "correct all the time" program. > >The trouble with formal verification methods is that they consume time >(for the analysis work) when you may well discover that the problem >wasn't specified well enough in the first place for formal >verification to actually do any material good. > >Having super-well-specified problems is extremely necessary when doing >"rocket science;" if it costs $1B to fire off a rocket, and you don't >get a second chance, it's necessary to do whatever up-front effort is >required to make sure the problem is super-well-specified. > >But there are a lot of cases where that level of effort is not >warranted, and it's NOT worth getting "super-detailed, super-correct" >specifications, and it's NOT worth various of the efforts. > >Where the CACM article has some things *right* is that there are >plenty of systems where it would be way too costly to reimplement them >in a buffer-overflow-immune language. People are not going to redo >everything in PL/1 or Ada just because they have better specified >string types. They don't have time. Perhaps the message of the article is that for future projects those languages would provide better outcomes. >-- >(format nil "~S@~S" "cbbrowne" "ntlug.org")