Re: [isabelle] Isabelle functions: Always total, sometimes undefined



Hi Joachim,


See £££ below..


________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Joachim Breitner <joachim at cis.upenn.edu>
Sent: 12 October 2017 20:57
To: cl-isabelle-users at lists.cam.ac.uk
Subject: Re: [isabelle] Isabelle functions: Always total, sometimes undefined

Hi,

Am Donnerstag, den 12.10.2017, 19:40 +0000 schrieb Andrei Popescu:
> Many people will probably agree with you when you declare
>
> > > Isabelle functions do not compute (unlike, say, Coq functions)
>
> However, I think stopping at this declaration means giving up too
> easily on what Isabelle/HOL (and HOL in general) have to offer w.r.t.
> certified programming.

Good point. I should add  section

### You can still compute with Isabelle functions


> Say you prove something about the source functions in each of these
> provers. Is the fact proved in Coq more relevant for the OCaml
> program than that proved in Isabelle?
>
> The answer is: No, provided some minimal precautions are taken about
> the specification and the code extraction setup. One can of course go
> into a discussion about the partial correctness restriction stemming
> from the additional flexibility of Isabelle/HOL's code generator
> (discussed by Haftmann and Nipkow), but this can be alleviated by
> removing that flexibility.

How can you achieve that?

£££ E.g., refraining from using that flexibility.  :- )

Coq users stress the point that when you extract from Coq to Haskell,
you know it terminates. And similarly, when you translate Haskell to
Coq, and Coq accepts it, then this is in a way a termination proof of
the Haskell code.

Can we say the same for Isabelle code extraction?

(I guess we can say the same for Haskabelle translation from Haskell to
Coq, because `fun` requires well-founded recursion.)

£££ We could achieve that, in principle, if we went through the trouble of automatically tracking executable specifications. In practice, I believe this is not such a big issue,: we can make sure this is the case by inspecting the definitions. Staying executable is easy -- the hard part is proving properties of the functions....

Andrei

-



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