Re: [isabelle] Overriding reason not to use single quote or camelcase in identifiers?



Makarius,

First, I have been influenced by your emphatic insistence, spoken in various ways, that we not use camelcase. Now I'm trying to come up with a solution for long identifiers that doesn't use underscores. Here, I resist the temptation to go into a lengthy discussion of my view of the aesthetics of the underscore. There's a lot of freedom with Isabelle; having figured that out, I now try to be flexible.

...a bigger issue is that I have to escape it [the underscore] in Latex. Right now, I'm not using the Isabelle Latex processing.
The Isabelle document preparation system will solve these problems for you. What are the reasons for not using it?

Last year, I worked on trying to use Isabelle to produce the PDF docs from the .thy files. In looking through the source of the tutorial, prog-prove.pdf, I can see the benefits of doing things your way, such as being able to put in hidden "oops"s.

However, there's a problem, and there's a complete show-stopper. You should keep in mind that I'm not willing to live without my Latex macros, especially for sectioning commands, which I tweak to create customized bookmarks. I think that in itself isn't/wasn't a problem, but it complicates things a little. Last year, my solution was to only use "text{*...*}", and none of the Isar sectioning commands.

PROBLEM: To be productive with Latex, you need to compile often, and be able to compile fragments. I don't remember if compile speed for a small theory was a problem, but to compile a theory fragment now, I'd have to write scripts to create temporary .thy files for the fragment, and these would have to import parts of the .thy that I'd be working on, so that Isabelle wouldn't choke on a logic error. It's just the hassle of switching over from what I use now, or, possibly, a big hassle.

SHOW-STOPPER: It's vaguely coming back to me, but I'm pretty sure that the show-stopper was my need for the Verbatim environment. I had to put it in a "text{*...*}" command, but "begin{Verbatim}" and "end{Verbatim}" are picky about what can be on the same line with them. I couldn't get rid of those errors, that I remember.

Anyway, I gave up and made the Isar subservient to the Latex in a tex file. I'm now back to making the Latex subservient to the Isar in a thy file by commenting out all the Latex, so that the file can be directly loaded into jEdit.

Right now, I can't spend more time on trying to make things look nice, at least done that way. The harder learning curve is Isabelle, and the prerequisite knowledge required to use it.

Generally, camelCaseWasInventedByPeopleWhoDidNotHaveUnderscoreAvailable
InTheireCharacterSet, probably around 1960/1970, before ASCII became universally accepted. Spacing between words improves readability, this was observed first about 3000 years ago...

There is the issue that using the underscore for spacing makes a name longer, but I'm seeing it your way, that spacing is important, and that capital letters are best used sparingly. And with a little work, I can probably come up with words that keep the name length down.

I'm kind of settling on a combination of limited camelcase use, and using the single quote character, ( ' ), to separate words in an identifier.

For example, I have the identifer "emS'is'unique". Below, I include a very fledgling theory where I don't know what I'm doing. It's to show some of my identifier naming.

I don't understand the motivation for that. The formal Latex generation of Isabelle works smoothly with things like @{text foo_bar}, @{thm foo_bar}, even @{ML foo_bar}.

You can also redefine the default isabelle latex macros to get a slightly different glyph for the underscore.

Here, I have to get into my opinions about mathematical writing, of which I'm more of a critique than a producer.

For me, at this point, there are two important driving principles, among others: 1) try to follow traditional, mathematical writing convention as much as possible, and 2) keep a clear distinction between the syntax and language of Isar, and the informal
         language of mathematics used to discuss, prove, define, etc..

The good news is that you were thinking about Isar over 10 years ago. Isar is sympathetic to tradition, with its structured proofs, the ability to abbreviate structured proofs, and with its standard mathematical symbols.

The breakdown, as I see it, comes with theorem names, function names, and constant names; that is, names in general. Formal, compound-word, long names, aren't a part of mathematical writing. So this requirement by programming languages that everything have a name doesn't fit with traditional-looking mathematical language in an unobtrusive way.

To describe the motivation for "emS'is'unique", consider this hypothetical sentence in my hypothetical book:

My dear reader, please consider what happens when /A/ is bounded by /b/.

Suppose formally that I've defined a function /is_bounded_by/. As a quick advertisement, I mention Slawomir's IsarMathLib.

http://www.nongnu.org/isarmathlib/

By looking at his document, I saw his use of infix notation such as "A {is disjoint with} B", which is shown on page 7. Okay. I like the idea, but I don't like curley braces for non-set use any more than I like underscores.

Here, I could stop writing and just say, "You know what, there is no perfect solution to trying to create spacing between words without only using spaces. Spaces look good when all you want is a simple space. All these other characters don't".

Well, back to my pontificating.

Alright, so you tell me that I can delay the decision on how to represent the underscore by using antiquotations such as @{text foo_bar}, and that I can substitute glyphs, probably very nice looking glyphs, for the underscore.

There are two problems. If I formally introduce /is_bounded_by/ into my Isar code, then that's exactly how I want to refer to it anywhere else, including in an informal discussion. As a total beginner, it was a source of confusion for me to see identifiers which had hyphens substituted for underscores. It's a non-issue now, but a 30-second concept can be a 1-weeker when I'm on my own, especially if I'm only in a discovery stage to try to determine if I want to go down a certain route.

The other problem is that I should make the "executive decision" now. There are only a few non-alpha-numeric characters available to use in an identifiers. Here's a list of me trying to name "is bounded by":

1) is_bounded_by
2) isBoundedBy
3) is'bounded'by

Really, if the phrase "is bounded by" was in a sentence in the middle of a paragraph, anything done to it would mess it up and break the flow of the sentence. Even italicizing it would mess it up.

The single ticks aren't looking so good to me at this moment. What I need to do is put the different names in the middle of a big paragraph, like in these sentences:

My dear reader, please consider what happens when /A is'bounded'by b/, or

    My dear reader, please consider what happens when /A is_bounded_by b/.

It's like recording music. You get up the next morning, and what you thought sounded good the night before, doesn't sound so good anymore. However, I think camelcase is out, for the most part.

Nothing's ever simple, though. What I see in jEdit, which is emS'is'unique, looks better because jEdit is using a fixed-width font. Thunderbird here is not using a fixed width font, so the ticks don't create enough space.

Regards,
GB
















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