Re: Verified compilers?

[phil.clayton@lineone.net]

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:
> 
> > 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.

See Donald MacKenzie's excellent book 'Knowing Machines' which makes extensive 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=c5YaHkcP6DEC&pg=PA160
(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 suggested.

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 asked
"So, what exactly is boolean algebra?"


> 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.

I assume you mean a complete CPU verified from design all the way to the gate level.  That would be interesting!

The hardware you are using right now almost certainly has some aspect of formal verification already, for example, Intel have been doing this for years.  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 
> 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.

I generally agree.  Certainly, much larger systems are now being verified but, when considering the actual advance, one should compensate for simply making use of greater computational resources.  Formal verification is fundamentally difficult so it is difficult to advance.  There are a lot of people out there trying.


> Which does not negate its value. Rather, I think it points to the fact 
> that there is much neglected ground, that could prove fertile.

I very much think so too!

Phil