*To*: Joachim Breitner <joachim at cis.upenn.edu>, "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Isabelle functions: Always total, sometimes undefined*From*: Andrei Popescu <A.Popescu at mdx.ac.uk>*Date*: Thu, 12 Oct 2017 19:40:40 +0000*Accept-language*: en-GB, en-US*Authentication-results*: spf=none (sender IP is ) smtp.mailfrom=A.Popescu@mdx.ac.uk;*In-reply-to*: <1507832320.1851.4.camel@cis.upenn.edu>*References*: <1507832320.1851.4.camel@cis.upenn.edu>*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:99*Thread-index*: AQHTQ4bZa9LyBZler02qKxocBmETKqLgk7zZ*Thread-topic*: [isabelle] Isabelle functions: Always total, sometimes undefined

Hi Joachim, 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. True, you can get non-computable behavior for the specifications of functions. But rather than saying that you cannot program in HOL, I would rather say that the traditional machinery developed in HOL-based provers includes a functional programming language, but currently does not (bother to) clearly single it out, as a subset of what can be specified. (Of course, singling that out would mean committing to intensional, extra-logical aspects -- which is always necessary when connecting logic with programming -- likewise, the termination property of a function written in Coq does not dwell in the Coq logic.) To see my point, consider the same OCaml program in the following two scenarios: 1) generated from an Isabelle/HOL function 2) extracted from a Coq function 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. Btw, for adequacy, both Coq and Isabelle would need to carefully consider that one reasons in a total logic about a program written in a "partial" environment, and rely on a form of "moral correctness" result (http://www.cse.chalmers.se/~nad/publications/danielsson-et-al-popl2006.html). Andrei ________________________________ 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 19:18 To: isabelle-users at cl.cam.ac.uk Subject: [isabelle] Isabelle functions: Always total, sometimes undefined Hi, based on repeated discussions and confusion when interacting with functional programmers and type-theory based theorem prover users, I wrote a blog post explaining how functions in Isabelle are different than functions in Haskell/Coq/etc, and what the deal is about undefined: http://www.joachim-breitner.de/blog/732 Please let me know if I say something wrong that should not be said like that on the Internet. Otherwise, feel free to share when you have trouble explaining these things to someone. Regards, Joachim -- Joachim Breitner Post-Doctoral researcher http://cis.upenn.edu/~joachim

**Follow-Ups**:**Re: [isabelle] Isabelle functions: Always total, sometimes undefined***From:*Joachim Breitner

**References**:**[isabelle] Isabelle functions: Always total, sometimes undefined***From:*Joachim Breitner

- Previous by Date: [isabelle] Isabelle functions: Always total, sometimes undefined
- Next by Date: Re: [isabelle] Isabelle functions: Always total, sometimes undefined
- Previous by Thread: [isabelle] Isabelle functions: Always total, sometimes undefined
- Next by Thread: Re: [isabelle] Isabelle functions: Always total, sometimes undefined
- Cl-isabelle-users October 2017 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