*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Berghofer's program extraction mechanism and code generation*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 23 Feb 2021 19:08:58 +0100*In-reply-to*: <fabf32c724e0bde5029abca6767f6364@cam.ac.uk>*References*: <fabf32c724e0bde5029abca6767f6364@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.7.1

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. Manuel 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) > https://www21.in.tum.de/~berghofe/papers/phd.pdf > > 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**

**Follow-Ups**:

**References**:**[isabelle] Berghofer's program extraction mechanism and code generation***From:*Dr A. Koutsoukou-Argyraki

- Previous by Date: [isabelle] Berghofer's program extraction mechanism and code generation
- Next by Date: Re: [isabelle] Berghofer's program extraction mechanism and code generation
- Previous by Thread: [isabelle] Berghofer's program extraction mechanism and code generation
- Next by Thread: Re: [isabelle] Berghofer's program extraction mechanism and code generation
- Cl-isabelle-users February 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list