Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy



On Wed, May 22, 2013 at 2:45 PM, Christoph LANGE <
math.semantic.web at gmail.com> wrote:

> 2013-05-22 14:26 Lawrence Paulson:
> > Coq and Isabelle/HOL are proof assistants, not programming languages. I
> can't imagine what gave you that idea. In Coq and Isabelle/HOL you write
> specifications, not code.
>
> Well, but there _is_ a notion of "programming" in Isabelle, given that
> it is based on a functional programming language, isn't it?


I would not put it that way.
Both Isabelle/HOL and <your favourite functional programming language> are
based on some flavour of lambda calculus. That's the connection.
However, there is no evaluation strategy specified for Isabelle/HOL terms,
and several constants don't have reducible definitions.
It's possible (and even common) to write uncomputable specifications in HOL
whereas you can't write anything uncomputable in a programming language.



>  I recall
> this earlier discussion on the title of the "programming and proving"
> tutorial:
>
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-November/msg00148.html
>
> Cheers,
>
> Christoph
>
> --
> Christoph Lange, School of Computer Science, University of Birmingham
> http://cs.bham.ac.uk/~langec/, Skype duke4701
>
> → Intelligent Computer Mathematics, 8–12 July, Bath, UK.
>   Work-in-progress deadline 7 June; http://cicm-conference.org/2013/
> → OpenMath Workshop, 10 July, Bath, UK.
>   Submission deadline 7 June; http://cicm-conference.org/2013/openmath/
>
>



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