Re: [isabelle] naming conventions (was "Want to use Rep_Integ or lifting after [quot_del] in Int.thy")
On 5/24/2013 11:18 AM, Makarius wrote:
You are a "writer" or "author" of formal source text, using a plain
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 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
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
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".
This archive was generated by a fusion of
Pipermail (Mailman edition) and