# 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.*