Email Gateway (Aug 19 2022 at 11:00): Email Gateway (Aug 19 2022 at 11:00):From: Makarius <makarius@sketis.net>
jEdit is a plain text editor. So you edit source text with it.
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.
Makarius
Email Gateway (Aug 19 2022 at 11:02):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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.
Makarius,
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
magic.)
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
specifier".
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."
Regards,
GB
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.Makarius
Email Gateway (Aug 19 2022 at 11:02):From: Gottfried Barrow <gottfried.barrow@gmx.com>
This email is one too many, other than I'd rather do this now, since the
thread has some momentum. Months from now, I don't want anyone to rehash
what's been said because I've decided to take the liberty to use
whatever vocabulary I want to use.
I'm settling on referring to Isabelle/HOL either as coding or as
programming, when I have a need to casually talk about it.
There's textbook style vocabulary that's used and being used in lots of
different places to label the languages of Isabelle, what Isabelle is,
and what you do when you're working with it. But I don't even see that
the developers are heavily using that type of language in day to day talk.
I'll take two words, "formalize" and "specification". To begin with,
they use too many characters. If you use "formalize", then you need to
use "formalization", which is even worse.
If I saw the Isabelle developers using these kind of words in the same
way that people talk about "programs" and "programming", then I suppose
I'd do it too, but am I suppose to look like a fool by heavily using
these formal sounding words when no one else has incorporated them into
their language similar to "program" and "programming"?
I'm willing to look the fool if there's a good reason, but I prefer to
minimize that kind of thing. And there's the huge issue of something
being practical. You can't expect me to have to use long, two word
phrases to refer to Isabelle code, or to refer to what I'm doing with
the Isabelle code.
This is not directed to anyone in particular, and my bi-monthly email
quota is up. You can blame Christian for badly influencing me.
Regards,
GB
Email Gateway (Aug 19 2022 at 11:02):From: Makarius <makarius@sketis.net>
On Fri, 24 May 2013, Gottfried Barrow wrote:
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.
The word "source" doesn't work in general.
2) When I'm editing a THY, am I "sourcing"?
You are a "writer" or "author" of formal source text, using a plain text
editor.
What is the terminology you would use yourself for latex sources? Latex
is also a programming language, but nobody "codes" papers, books, theses
etc. with it.
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."
In the worst case, something like "user of Isabelle" will always work.
Makarius
Email Gateway (Aug 19 2022 at 11:02):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I don't think so Makarius. I'm still rebelling, and Larry has never
officially backed out of saying that Isabelle/HOL is a programming language.
There is "program", "programming", and "programmer", and "code",
"coding", and "coder", where right now I'm preferring "programming".
If someone asks, "What you do for a living?", do I say, "Well, I don't
get paid for it, but I'm a writer who writes writings."
Wouldn't they be more likely to say or think, "Oh, so you write novels,
or maybe you're a journalist?"
I am one over my bi-monthly quota of emails, but this is about the future.
Again, this is not directed at anyone in particular, but in the future,
if I'm corrected for using "programming" in relation to Isabelle/HOL, I
will reference the thread where Larry calls HOL a programming language,
and I will reference this thread.
I will then say, "then please give me three words to replace 'program',
'programming', and 'programmer'".
Me doing that will be much better than writing lengthy emails, as I have
been doing.
My goal is to become a very competent Isabelle/HOL "programmer". It's
the only "programming language" I use at this time. I do some scripting
and text processing, but there's already established vocabulary for
those, which would be "script" and "scripting", and "text" and "text
processing".
As a rebel, I can't see that it's reasonable for me to have to
frequently resort to long phrases like "I write formal source text".
Regards,
GB
Email Gateway (Aug 19 2022 at 11:02):From: Gottfried Barrow <gottfried.barrow@gmx.com>
So when the use of a language or product is prolific, such as with LaTeX
or Java, then using the name is enough to define what you do.
"What do you do?"
"I do Oracle."
If the use of Isabelle was prolific, then the use of "Isabelle/HOL"
would set the context. But Isabelle/HOL is relatively unknown in the
programming world, and it wouldn't solve my need for a word like
"programmer". Or maybe it would.
"What do you do?"
"I write HOL source."
But it's not prolific. So to say, "I write HOL source", is to invite the
question, "Oh, that sounds interesting. But what is that exactly?"
Instead of,
"What do you do?"
"I'm a programmer."
"Oh." (Their eyes shift around, looking for someone else to talk to.
That's good. You didn't feel like talking about it either.)
Regards,
GB
Email Gateway (Aug 19 2022 at 11:12):From: Christian Sternagel <c.sternagel@gmail.com>
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
Email Gateway (Aug 19 2022 at 11:12):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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
Last updated: Apr 26 2024 at 16:20 UTC