[isabelle] naming conventions (was "Want to use Rep_Integ or lifting after [quot_del] in Int.thy")

Dear Gottfried,

my 2 cents concerning naming (everyone: please correct and/or complete):

- Coq is a proof assistant (or interactive theorem prover)

- Isabelle is a generic proof assistant, where Isabelle/HOL is its instance for Higher-Order Logic. Thus I would call Isabelle/HOL a proof assistant (omitting the term "generic"; also "interactive" from "interactive theorem prover" is sometimes omitted, but I prefer not to do so).

- The main purpose of proof assistants, as their name suggests, is to assist the user to make proofs. That is, *proving* as opposed to *programming* is the main thing.

- In the recent literature developing a theory (or a proof for some statement) A in a proof assistant is called: mechanizing A, or formalizing A, or certifying A, ... but never programming A



On 05/22/2013 11:02 PM, Gottfried Barrow wrote:
On 5/22/2013 8:26 AM, 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.

Larry Paulson


My general rule is to never use emoticons, but rules have their exceptions.

You gave me that idea :). As to acronyms such as "lol", even under these
circumstances, they're still unacceptable.

This is the specific email:


This will contain the thread:


I was just starting to decide that under certain contexts, I could refer
to Isabelle/HOL as a programming language, because it's just a lot
easier to use that phrase sometimes, whereas, according to your specific
clarification in the email linked to above, Isabelle/Pure and
Isabelle/Isar are never to be called programming languages, so I try to
use "proof language" or "source language" when referring to them, even
when I know others might not get my point.

One of my other recent emails to the list spawned some private chatter
in which I referred to HOL as a programming language, which resulted in
a similar response to yours,  which paraphrased would be, "What is this
programming language you're talking about in reference to HOL?"

That's why I had easy access to the links above, because I thought I had
the perfect, authoritative reference to explain that Isabelle/HOL is a
programming language, where Pure and Isar aren't.

In an attempt to use safe, correct vocabulary, I've resorted to using
"coding language" when trying to refer to the whole Isabelle family of
languages. At some point, there's a need for phrases, like, "I'm
programming with Isabelle/HOL", or, "I'm coding with Isabelle". Like I
say, "coding" has become my word of choice to replace "programming".

Anyway, I'm happy to try and use the official vocabulary correctly.
There are a ton of interwined languages with Isabelle, so I give up and
get lazy sometimes, and just say "programming language".

As to Coq, it seems to me if I can call Isabelle/HOL a programming
language, then I can call Coq a programming language. That's just an
aside. I'd be happy to use any official Coq vocabulary to use to refer
to Coq.


On 22 May 2013, at 14:16, Gottfried Barrow<gottfried.barrow at gmx.com>

Thanks for your comment. I was comparing the formal, textbook
construction of the integers, as in what you're listing, to concrete
implementations of integers in programming languages, such as Coq,
Isabelle/HOL, Haskell, or any other language, old or new, but
especially new.

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