Re: Verified compilers?

["Randy Brukardt" <randy@rrsoftware.com>]

"Stuart" <google_news@palin-26.freeserve.co.uk> wrote in message 
news:15276255.3865.1331124143041.JavaMail.geo-discussion-forums@vbze11...
On Tuesday, 6 March 2012 01:27:25 UTC, Randy Brukardt  wrote:
...
> I admit I have not read the report yet - so I am unaware of the scope of 
> the 'formal verification';
> and Randy's post does point out other areas where errors creep into the 
> compilation process.
> That said, there is still an issue in safety-critical applications of 
> constructing a robust and
> compelling safety case, particularly covering the compilation process. 
> This would seem to be
> something that would aid in such cases.

I thought about that some after posting my reply. I probably was a bit too 
flippant. The real problem is that the only languages that can practically 
be verified are extremely simple, and I suspect it usually would be a bad 
idea to code large systems in such languages. (All of the advantages of a 
language like Ada -- or even C++ -- would be thrown away. After all, that's 
my complaint about SPARK, and this would be many times worse.)

...
> Whichever stage of the compilation process is at fault, [in my experience] 
> there are usually
> a number of target code faults associated with fairly mature compilers and 
> these cases have
> to be managed by the safety case and development processes.

True enough. But I don't think that it would be all that practical to verify 
an entire compiler for a real programming language. Moreover, I doubt that 
it would take any special architecture to do so, just a reasonable 
partitioning of concerns. It surely would be "easy" to verify the 
translation of our intermediate code to machine code (particularly if small 
simplifications were made in both; a formal definition would be needed for 
the intermediate code, but that would not be hard to do - it's already 
defined by Ada source code and carefully documented in English). It probably 
would be practical to verify the intermediate code transformations of an 
optimizer (not ours, however). Verifying the translation of raw syntax to 
intermediate code would be harder, and would mainly depend on a formal 
definition of the source language (which as noted, would be impossible to 
provide for any real language; part of the problem being that no human could 
understand it well enough to know if it is right -- so would verifying that 
it is translated properly really provide any benefit??).

> Getting people with the experience at both the high-level source and 
> low-level target code
> to review compilation issues is becoming increasingly difficult.  A 
> technique that provides
> alternatives in verifying the compilation process are attractive.

Understood, but as noted I'm dubious that this would really help. You could 
verify *some* language, but whether it really was the same language that you 
wanted would be impossible to tell. I suppose if you could hook up a 
SPARK-like verifier to it, you could see if your program did what you want 
based on the formal description  -- whether that actually matched the 
expected semantics or not -- but that would require describing the intended 
outputs of your program in the language of the formal description, and I'm 
dubious that you could understand *that* well enough to tell if it really 
did what you want.

And if you succeeded in doing that, you no longer need the program itself --  
it's just an artifact, you might as well directly translate the formal 
specification into code -- at which point you have to start the entire cycle 
again. (Can you tell that I think trying to verify everything is a waste of 
time, not matter what it is??)

Anyway, it's certainly true that some programming problems need 
extraordinary measures. And I suppose for those people, this sort of thing 
will appear to be a new silver bullet. But of course there is no silver 
bullet for programming - it's hard, it is going to remain hard, and worrying 
too much about the compiler when the source program is hardly verified at 
all makes little sense.

                                                        Randy.