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

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>  wrote:

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.