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,5412c98a3943e746 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.220.229 with SMTP id pz5mr3969991pbc.5.1331338514000; Fri, 09 Mar 2012 16:15:14 -0800 (PST) Path: h9ni8072pbe.0!nntp.google.com!news2.google.com!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail From: phil.clayton@lineone.net Newsgroups: comp.lang.ada Subject: Re: Verified compilers? Date: Fri, 9 Mar 2012 15:59:21 -0800 (PST) Organization: http://groups.google.com Message-ID: <3398270.1725.1331337561115.JavaMail.geo-discussion-forums@vbgx21> References: <15276255.3865.1331124143041.JavaMail.geo-discussion-forums@vbze11> <87d38nv4zf.fsf@adaheads.sparre-andersen.dk> NNTP-Posting-Host: 2.27.126.221 Mime-Version: 1.0 X-Trace: posting.google.com 1331338513 11473 127.0.0.1 (10 Mar 2012 00:15:13 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sat, 10 Mar 2012 00:15:13 +0000 (UTC) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=2.27.126.221; posting-account=v7gx3AoAAABfjb9m5b7l_Lt2KVEgQBIe User-Agent: G2/1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Date: 2012-03-09T15:59:21-08:00 List-Id: On Friday, March 9, 2012 1:56:34 PM UTC, Brian Drummond wrote: > On Thu, 08 Mar 2012 23:38:39 +0000, Bill Findlay wrote: >=20 > > On 08/03/2012 10:23, in article jja1b4$8q1$1@dont-email.me, "Brian > > Drummond"=20 > wrote: > >=20 > >> On Thu, 08 Mar 2012 10:04:04 +0100, Jacob Sparre Andersen wrote: > >>=20 > >>=20 > >>> Oh. And who verifies that the silicon is correct? > >>=20 > >> VIPER. > >>=20 > >> en.wikipedia.org/wiki/VIPER_microprocessor > >> www.cl.cam.ac.uk/techreports/UCAM-CL-TR-104.pdf > >=20 > > Was the 'proof' of VIPER not later shown to have missed serious faults? >=20 > Quem vedisti pastores? >=20 > That must be the "controversy" hinted at on Viper's Wikipedia page.=20 > Unfortunately, apart from the Dick Pountain article in Byte, I don't know= =20 > anything about the VIPER, so any further info would be appreciated. See Donald MacKenzie's excellent book 'Knowing Machines' which makes extens= ive reference to the VIPER case. (It is a fairly unique example.) The short chapter covering the VIPER fiasco can (except for the first page)= be read here: http://books.google.co.uk/books?id=3Dc5YaHkcP6DEC&pg=3DPA160 (Don't let that stop you buying the book though!) Ultimately the problem seems to be that expectations were set too high: the= formal proofs did not say as much about the actual hardware as people may = have been led to expect and the commercial prospects were not as great as s= uggested. I used to work in the same team as one of the VIPER developers, though many= years after VIPER, and it is always interesting to hear parts of the story= . One favourite is an early meeting with the lawyers. They sat down and a= sked "So, what exactly is boolean algebra?" > It would be interesting to see verified hardware : maybe even VIPER=20 > revisited with newer proof tools; and to see if something more like a=20 > real CPU - say an ARM1 or 2 (let's not be too ambitious!) - would be=20 > verifiable these days. I assume you mean a complete CPU verified from design all the way to the ga= te level. That would be interesting! The hardware you are using right now almost certainly has some aspect of fo= rmal verification already, for example, Intel have been doing this for year= s. There is plenty of information out there discussing the issues, e.g. http://www.cl.cam.ac.uk/~jrh13/slides/types-04sep99/slides1.pdf > While it amuses me to see SPADE references so close to the surface in=20 > SPARK, it does also make me question how much progress has been made in= =20 > formal verification in the last quarter century. Gut feel says, more than= =20 > AI and flying cars, but not much. I generally agree. Certainly, much larger systems are now being verified b= ut, when considering the actual advance, one should compensate for simply m= aking use of greater computational resources. Formal verification is funda= mentally difficult so it is difficult to advance. There are a lot of peopl= e out there trying. > Which does not negate its value. Rather, I think it points to the fact=20 > that there is much neglected ground, that could prove fertile. I very much think so too! Phil