[isabelle-dev] consts_code wfrec (Re: Code generation in Isabelle)
krauss at in.tum.de
Sun Jul 24 21:50:44 CEST 2011
> Aside: On page 232 of the above-mentioned manual there is an example
> about const_code wfrec. The same is still used here in MicroJava:
> The source says "Code generator setup (FIXME!)".
> The changelog says: "no consts_code for wfrec, as it violates the "code
> generation = equational reasoning" principle" (before it was in
Here is the long version of eee4fa79398f:
Recall that our notion of "correctness of code generation" is that any
evaluation in the generated code could theoretically be replayed by
equational reasoning within the logic. This is the basis of the
"evaluation oracle", which proves statements by evaluating them to true.
The attached theory shows that this is inconsistent with the above
consts_code declaration for wfrec. I have this since 2007 and showed it
to a bunch of people at that time. The present form uses neither recdef
nor function, which clarifies the issue a bit. In a nutshell, the
unconstrained evaluation lets us "prove" things that are not true in the
> Does that mean there is something utterly wrong with MicroJava?
Not deeply, since MicroJava does not use the evaluation oracle, so it
does not matter if code generation is sound or not. Nevertheless it
would be good to get rid of it and to make MicroJava executable in some
other way. Also note that this declaration (by coincidence) is not
possible with the new code generator, since that does not seem to
support the funny "question mark notation" for silently dropping the
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
More information about the isabelle-dev