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.134.225 with SMTP id pn1mr2475333pbb.7.1331301395044; Fri, 09 Mar 2012 05:56:35 -0800 (PST) Path: h9ni6415pbe.0!nntp.google.com!news2.google.com!goblin2!goblin.stu.neva.ru!aioe.org!eternal-september.org!feeder.eternal-september.org!mx04.eternal-september.org!.POSTED!not-for-mail From: Brian Drummond Newsgroups: comp.lang.ada Subject: Re: Verified compilers? Date: Fri, 9 Mar 2012 13:56:34 +0000 (UTC) Organization: A noiseless patient Spider Message-ID: References: <15276255.3865.1331124143041.JavaMail.geo-discussion-forums@vbze11> <87d38nv4zf.fsf@adaheads.sparre-andersen.dk> Mime-Version: 1.0 Injection-Date: Fri, 9 Mar 2012 13:56:34 +0000 (UTC) Injection-Info: mx04.eternal-september.org; posting-host="DkTdSjxOCm6DqG+Uf7eArg"; logging-data="20514"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18dUzwY8i1KAN9jdCoqPMvnBqER2OYJ1M0=" User-Agent: Pan/0.134 (Wait for Me; GIT cb32159 master) Cancel-Lock: sha1:70jSifeT8pSXzhAvb4vwYev2AFo= Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Date: 2012-03-09T13:56:34+00:00 List-Id: On Thu, 08 Mar 2012 23:38:39 +0000, Bill Findlay wrote: > On 08/03/2012 10:23, in article jja1b4$8q1$1@dont-email.me, "Brian > Drummond" wrote: > >> On Thu, 08 Mar 2012 10:04:04 +0100, Jacob Sparre Andersen wrote: >> >> >>> Oh. And who verifies that the silicon is correct? >> >> VIPER. >> >> en.wikipedia.org/wiki/VIPER_microprocessor >> www.cl.cam.ac.uk/techreports/UCAM-CL-TR-104.pdf > > Was the 'proof' of VIPER not later shown to have missed serious faults? Quem vedisti pastores? That must be the "controversy" hinted at on Viper's Wikipedia page. Unfortunately, apart from the Dick Pountain article in Byte, I don't know anything about the VIPER, so any further info would be appreciated. It would be interesting to see verified hardware : maybe even VIPER revisited with newer proof tools; and to see if something more like a real CPU - say an ARM1 or 2 (let's not be too ambitious!) - would be verifiable these days. While it amuses me to see SPADE references so close to the surface in SPARK, it does also make me question how much progress has been made in formal verification in the last quarter century. Gut feel says, more than AI and flying cars, but not much. Which does not negate its value. Rather, I think it points to the fact that there is much neglected ground, that could prove fertile. One area, directly germane to the question above, is that there is a lot of commonality between the SPARK subset of Ada, and the synthesisable subset of VHDL, probably because both share the need for static elaboration of resources. I would like to see this exploited in several ways, whether as SystemAda (surely a better alternative to SystemC) for SW/HW co-verification or ESL design, or as SPARK-like proof tools applied to VHDL. VHDL and Ada seem to be following separate but convergent evolution paths (e.g. VHDL has conditional and case expressions, Ada will. Ada has inheritance, VHDL doesn't ... yet) and formal proof would appear to be equally applicable to suitable subsets of both. > (BTW nice to see that someone else remembers the Rekursiv.) (well I know a little more about THAT!) There was a lot of interesting hardware at the time. I was intrigued by the similarity between Transputer and Lilith instruction formats, which might be worth re-examining where code density (or making it fit in cache) is important. - Brian