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



Christian,

There's no person on the face of the Earth more appropriate to continue this conversation with than with you. So now, having intentionally tried to make Larry suffer less, I now make you suffer.

There's a certain forum in which I deemphasized Isabelle as a "programming language", a point which you countered, a counterpoint which I partially countered.

As many times, what I reject, after having some time to think, I then, in some form, embrace. And so, my mental investigations, even now, is in trying to determine whether "programming language" can be legitimately applied to Isabelle/HOL, where I'm leaning towards saying "yes", though that doesn't mean I'll use the label anymore.

Having had my say with too many emails on this, I am now only interested in choosing vocabulary for Isabelle for pure, practical reasons.

Without explaining any of the thought process that's led to this, I seek one word, where the following describes some of the criteria:

1) What is one word which I can use to label the many languages that are used in what I see in jEdit?

2) This word needs to general enough to describe the main languages that I see: Pure, Isar, and Isabelle/HOL.

3) This word needs to be able to be used as a noun and a verb.

4) This word, as a noun, needs to describe what someone might want to call me.

5) This word, as a verb, needs to describe I am doing when I use Isabelle as a language.

6) This word needs to be acceptable by the experts as being technically correct.

7) This words needs to have meaning to programmers who know nothing about Isabelle as a language.

So the word "programming", because it's been used for years, and has accumulated many connotations, doesn't work.

Below, you give me vocabulary, and I am happy to follow the lead of the official documentation, the principal developers, and the rest of the professional developers, like you.

But, as I said, my pursuit of a word is for everyday, practical usage.

To make a long story short, the word is "code".

Isabelle has source code files with the extension "thy".

1) If they are source code files, then what I'm looking at in jEdit must be code.

2) If I'm editing code in a THY file, then it must be I'm coding.

3) If I ever get good enough at coding with the many languages of Isabelle, then it must be that I'll be a "coder".

4) "Code" has no connotational requirement that anything be executed.

5) It doesn't have to be a recipe, as with programs.

6) "Code" is merely information that is "encoded".

So, at this point, seeing that "code", though commonly used, hasn't been totally corrupted, maybe the proof assistant community can usurp the word for their purposes.

Why? If leading authorities don't give the masses a practical word to use for something, they'll choose their own word. Compare Latin to Vulgar Latin. Language usage is heavily determined by anarchy.

Hypothetical scenario: I have 350 characters to make a comment on a forum. Do I say, "When I myself am writing formal specifications with Isabelle..."

Yes, I do, if I'm trying to be the benevolent educator, taking advantage of what can be a teachable moment.

However, no, I don't, not if I'm at 400 characters. The phrase "writing formal specifications with Isabelle" becomes "coding in Isa".

I've just mentioned an upside to the word "code". It's four letters. I can't think of a three letter word at all to replace "code".

I'll check out of this thread on what is good or bad vocabulary.

Regards,
GB

On 5/22/2013 9:03 PM, Christian Sternagel wrote:
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

cheers

chris

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

Larry,

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:

http://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/msg00034.html


This will contain the thread:

http://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/thread.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/thread.html>


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.

Regards,
GB





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 MHonArc.