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.

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.


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