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"
To my taste, the attempt to see Mizar articles as potentially
computational is even more artificial for that particular proof checker.
This archive was generated by a fusion of
Pipermail (Mailman edition) and