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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.