Re: State of the compiler market

[antispam@math.uni.wroc.pl]

Paul Rubin <no.email@nospam.invalid> wrote:
> antispam@math.uni.wroc.pl writes:
> >> team up with the CompCert guys and make a verified Ada compiler.
> > Maybe a blasphemy here, but if you go trough full formal verification
> > does Ada offer significant advantages over C or C++?
> 
> You mean if the application is verified?  Depends on what has been
> verified, I suppose ;).  The idea of CompCert is just that the compiler
> is verified so there's less worry about compiler bugs.  That's
> independent of the verification processes you might use for your
> application.

Once you have verified compilation process it is natural to
go for full formal verfication, from specification to
machine code.  Actually, given that formal verfication
of chips is quite advanced once can go for verfication
up to logic gates.  This is it should be possible to
exclude logic bugs in chips.
 
> > L4.sec guys deliver code via C and apparently this did
> > not hamper their efforts.
> 
> SEL4 is apparently around 10 KLOC of C and 480 KLOC of Isabelle/HOL
> proofs, and the C was apparently produced (not sure whether manually or
> automatically) by some kind of derivation from an executable
> specficiation written in Haskell.  I haven't actually read the SEL4
> papers but that comes from a quick glance.  They are accessible from
> here:  http://ts.data61.csiro.au/projects/seL4/

I read one of the papers and they write that translation
from Haskell to C was done by hand.  They state that
they used subset of Haskell avoiding features hard
to translate to lever level language, so presumably
one could create appropriate translator.  OTOH IIRC
according to their time report writing C code took less
than 15% of total time, so it is possible that doing
translation manually was faster than developing
translator program.

> > Ada strength is in intermediate area where better checking in compiler
> > and safer programming practices lead to faster delivery of reasonably
> > good program.
> 
> This is reasonable to say.  Also Ada's verification tools like SPARK
> supply more automation than what's available for C as far as I can tell.

Few years ago I talked with guy from Microsoft Research doing
formal verfication.  He claimed that their tools checked
more things than SPARK.  And also he claimed that they
needed less annotations (he said that methodology of
SEL4 required about 8 times more annotations than
required by Microsoft tools).  Main point was availability
of quite strong proof engine and automatic generation
of intermediate conditions.

-- 
                              Waldek Hebisch