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



On Wed, 22 May 2013, Lawrence Paulson wrote:

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.

I agree with that, although the "marketing" of proof assistants in the last 10 years or so has moved in a different direction. Today most people think of Coq as some dependently typed functional programming language, and the Agda is emphasizing the programming aspect even more.

My own terminology is mainly about "formal languages" and "formalization" of any kind. For example, the formal proof language of Isar is used to write formal proofs, not to "program" nor to "implement" proofs.

Isabelle/ML and Isabelle/Scala happen to be programming languages just by accident, so you can use them to program things. The Isabelle document preparation language (formal latex) also happens to be computationally complete, but nobody would say to "program" / "implement" / "code" some text for a paper or book.


Interestingly, the computational or non-computational aspect of languages often causes additional confusion for licensing. E.g. see the discussion in the paper about "Licensing the Mizar Mathematical Library" http://arxiv.org/abs/1107.3212

To my taste, the attempt to see Mizar articles as potentially computational is even more artificial for that particular proof checker.


	Makarius




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