From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>

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

From: Manuel Eberl <eberlm@in.tum.de>

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

smime.p7s

From: Tjark Weber <tjark.weber@it.uu.se>

This is ameliorated by the fact that lemmas often have no

"computational content": their proofs do not affect the extracted

program. Therefore Isabelle's automation may still be useful in

(possibly large) parts of a formalization intended for program

extraction.

Best,

Tjark

När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

Note that code generation using extraction from proofs works in two steps:

a) The extraction part: Turning a proof into a set of definitions and

corresponding equational theorems in Isabelle/HOL

b) The code generation part: Turning those theorems into executable

programs.

Hence there is no fundamental difference: both approaches rely on a

regular code generator, although that has been replaced in the meantime.

Personally I tend to view proof terms in Isabelle as a device to bolster

the logical foundations. The code generation examples in the

distributions are nice demonstrations – but the mechanism so far has no

impact on practical applications.

Cheers,

Florian

signature.asc

Last updated: Dec 08 2021 at 09:20 UTC