2011/6/21 Jason Dagit <dag...@gmail.com> > On Tue, Jun 21, 2011 at 3:31 AM, Uli Kastlunger <squar...@gmail.com> > wrote: > > Hello Haskell fellows, > > > > recently there has been a huge progress in generating real programs by > > specifying them in interactive theorems prover like Isabelle or Coq, in > > particular a verified C Compiler has been generated out of a > specification > > in Coq [0]. Furthermore it is often stated, that it is easier to reason > > about functional languages. So in my opinion there are two approaches > > building verified software (e.g. in case of compilers: verify that the > > semantics of a high-level language maps correctly to the semantics of a > > low-level language). > > > > (0) Programming in any language and then verifying it with an external > > theorem prover > > (1) Specifying the program in a proof language and then generating > program > > code out of it (like in the CompCert project) > > > > I think both ideas have their (dis)advantages. The question is, which > > concept will be used more frequently? In particular how hard would it be > to > > build something like CompCert the other way around (in this case writing > a C > > compiler in SML and proving its correctness?) > > Proving the correctness of a C compiler is quite a challenge > regardless of how you write the compiler. The reason there is that > you need a well-defined version of C so that you have a spec for the C > compiler that can be used in formal methods approaches. > > Assuming you've done that, then it seems like SML would lend itself > just fine to being your implementation language. Tools like > Isabelle/HOL could be used as your external theorem prover. > > If your compiler is fully verified then that's great news but you > could still write buggy programs with it. Likewise, you could have a > proven your program is correct with respect to the formal semantics of > the language and your program specification but then used a buggy > compiler. So it seems to me that not only do the two approaches you > outline have different advantages but they are solving different and > closely related problems. > > I'm no expert with compcert, but as I understand it their approach is > to only do semantic preserving changes to the program at each step in > the translation from C source to binary. I'm not sure what they used > as their specification of C and it seems like the correctness of their > approach would still depend on a spec. > > I hope that helps, > Jason >
First, a small correction to CompCert: I got this wrong, it generates Caml Code not SML Code. You are right, to do a verified Compiler, you need a specified Version of C and also a specified Version of you target assembly language. But the question is, if it is then more applicable to write your Compiler in a language like Haskell and then verify it, or if you do it the other way around, use a specification language which can generate verified code. br, uli
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
