Re: [isabelle] Berghofer's program extraction mechanism and code generation

I don't know terribly much about Berghofer's work, but I'm fairly
certain it has absolutely nothing to do with how the code generator works.

I think Berghofer's approach is closer to what people do e.g. in Coq:
using the Curry–Howard isomorphism to get code from the proof terms.

My impression from a distance that Berghofer's implementation is a very
impressive accomplishment, but one that has not been used for anything
but small examples so far.

One big problem is that (unless I misunderstood something) it only works
as long as you don't use any non-constructive reasoning (i.e. no axiom
of choice, no proof by contradiction).

However, one of the big strengths of Isabelle/HOL is automation, and
none of the automation cares about constructive vs non-constructive, nor
does it care about keeping proof terms small (because normally proof
terms are not stored anyway). Thus, if you use automation, Berghofer's
approach will either not work at all (because the automation used
something non-constructive somewhere) or run into performance problems
or give you horribly bloated code (because the automation produced huge
and overly complicated proof terms).

And these problems only become bigger if you apply it to bigger examples.

The code generator, on the other hand, works by having very tight
control over what code is produced: things like equational and recursive
definitions work out of the box, anything else (quantifiers, choice,
inductive predicates, abstract types, quotient types) requires some
extra work (e.g. proving code equations, running "code_pred", …).

Basically, the code generator works by translating equations in HOL into
"equations" in ML/Haskell/Scala/etc. and "pretending" that the meaning
is the same (which is somewhat justified). And anything constant that
isn't specified by a simple equation has to be brought into that form by
the user (by supplying code equations).

Hope that helps – if I said anything wrong, I'm sure someone will
correct me.


On 23/02/2021 18:56, Dr A. Koutsoukou-Argyraki wrote:
> Dear all,
> I'm interested to understand if/how Stefan Berghofer's program
> extraction mechanism
> for Isabelle as developed in his PhD thesis (in the sense of obtaining
> realizers)
> is related to the current approaches for code generation from Isabelle/HOL.
> It would be great if you could share your insights.
> Many thanks in advance!
> Angeliki

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.