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.
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
On 22 May 2013, at 14:16, Gottfried Barrow<gottfried.barrow at gmx.com> 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