Re: Verified compilers?

[Brian Drummond <brian@shapes.demon.co.uk>]

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" <brian@shapes.demon.co.uk> 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