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.

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






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