Re: [isabelle] naming conventions (was "Want to use Rep_Integ or lifting after [quot_del] in Int.thy")
On 5/23/2013 6:32 AM, Makarius wrote:
On Wed, 22 May 2013, Gottfried Barrow wrote:
1) What is one word which I can use to label the many languages that
are used in what I see in jEdit?
jEdit is a plain text editor. So you edit source text with it.
See, it's not like I'm wanting to rebel on the words I'm going to choose
to start referring to Isabelle, but my needs aren't the needs of 99.9%
of the people who use Isabelle, and I am a member of the masses who will
corrupt the language if given vocabulary that is too hard to use.
I can program some, but I'm not a programmer. There was a point at which
I would have been a programer who wrote diagnostic software for embedded
controllers, but that fell by the wayside.
The word "source" doesn't work in general.
1) In conversation, do I say, "The source on line 300 of Int.thy..."?
(That's not too bad.)
2) When I'm editing a THY, am I "sourcing"?
3) If I get good at using the languages of Isabelle, am I a "Isabelle
sourcer"? (Not to be confused with a sorcerer, one who works software
I can try other words, like "specification", "formalize", and "proof".
1) "The specification on line 300 of Int.thy...".
2) "I myself, when specifying in Isabelle...".
3) "Someday, I might have earned the right to be called an Isabelle
Will there come a day when I want to be called a "formalizer" or a
"prover"? Only if you take the lead and start calling yourself a
"formalizer" and a "prover" so that I have links to refer to when
someone says, "Uh, you're a formalizer, you say?"
In Isar, with my awareness raised, and because vocabulary used in
isar-ref.pdf, I can see that Isar is a "source language" in general, and
parts of it are a "proof language", so I've figured out the vocabulary I
need to use when referring to Isar.
However, it's not a simple thing to try and talk about the combination
of Isabelle/Pure, Isabelle/Isar, and Isabelle/HOL.
1) In a THY, you're always in Isar the source language, but from one
line to another, you may or may not be in Isar the proof language.
2) On a particular line, you are always in Isar the source language, but
your syntax may or may not be Isabelle/HOL syntax.
3) An outer syntax keyword may be both an Isar keyword and Isabelle/HOL
keyword, or it may only be an Isar keyword. One may need to look in
isar-ref.pdf for the characters "(HOL command)" to find out.
I suppose all this complexity is what gives Isabelle its power and
flexibility, but I'm talking about the need for the masses to engage in
polite conversation and not be saying things like, "You really should
try Isabelle, Joe. I've become an Isabelle specifier myself."
Isabelle/jEdit augments that a little bit to add formal markup from
the meaning of the source text right into the text view. This conforms
to the traditional notion of theory source text that you are editing,
while the prover is telling about the formal content of it.
Anyway, there is this old joke about "HTML as programming language".
For plain HTML 1/2/3/4 it was indeed a rather bad joke. For HTML5 I
am not sure anymore -- too many computational add-ons as it seems.
This archive was generated by a fusion of
Pipermail (Mailman edition) and