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



On Tue, 3 Jul 2012, Gottfried Barrow wrote:

I've read the style guide in implementation.pdf, so I've read and seen that the preferred identifier naming scheme uses the underscore character "_". However, I don't like how it looks, but a bigger issue is that I have to escape it 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?

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 -- the ancient Phoenicians and early Greek writers did not know it yet. Classic fonts are also designed to have capitals in front of words only, not in the middle. You can see this especially in the Computer Modern fonts of LaTeX.

Even though our classic (Unix) standard of separating words by underscore has been there from the beginnings (1980-ies/1990-ies), one reason why it was made more explicit in recent years might be the advent of good typographic screen fonts like Bitstream Vera. Then the rules for proper typography become more important to screen display.


So why do many younger people still consider camel case as standard? My theory on the main historical events is that:

  * Xerox PARC that introduced the legendary Xerox Star computer system
    with bitmap display, mouse, object-oriented programming for GUIs in
    the 1970-ies was one of these labs living in the IBM-tradition of not
    having "_" on the keyboard nor in the character set.  So the classic
    workaround to use camelCaseAsAnApproximation was employed.  (You can
    still see that in the "Axiom" programming language, for example, which
    lacks "_" by default.  It is from a genuine IBM lab.)

  * Apple copied that to make the Lisa and Macintosch.

  * MS copied that to make Windows.

  * Almost everybody else copied that as well.

What remains are a few ancient guys like in the Isabelle, Coq, OCaml
communities, who did not submit to that invasion.



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.


(I haven't figured out if the unicode characters in an email like this show up correctly in other's email readers.)

I would say that should work out in practice, I am doing it myself all the time now. Strictly speaking one cannot expect 100% reliability of unicode transmission, but such mail threads are not for achiving of 100% correct formal sources (unlike a repository which has to be more authentic).


	Makarius





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