Re: [OTish] Proving compiler algorithms implement same semantics as language specs? [was Re: [PATCH][RFC] Re-implement restrict support]

["Joseph S. Myers" <joseph at codesourcery dot com>]

On Tue, 23 Jun 2009, Dave Korn wrote:

>   I'd guess there has to be some way in formal logic or propositional calculus
> by which we could take descriptions such as Richard's above, and the
> description of restrict semantics in the standard, and reduce them each to a
> pile of propositions that we could feed into a theorem-proving system and get
> it to prove they were identical.

Norrish's thesis <http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-453.pdf> 
formalised a subset of C90 in HOL, but I don't know what developments 
there have been in this area since 1998.  It may not always be clear what 
the standard means, and I also quote Norrish:

    This ... tells us nothing about the quality of our semantics with 
    respect to the original specification .... Better would be to have the 
    specification of the semantics inspected by another individual who was 
    both familiar with the fine details of the ISO standard, and the 
    techniques of operational semantics.  Unfortunately, such people are 
    hard to find, which is rather an indictment of the divergence between 
    theory and practice in computer science.

Theorem proving systems have been successfully used for IEEE 
floating-point algorithms, where the intended semantics are more precisely 
defined and better understood.  I believe that following the Pentium FDIV 
bug Intel now uses formal verification for the floating-point algorithms 
in its processors.

-- 
Joseph S. Myers
joseph@codesourcery.com