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:
In the worst case, something like "user of Isabelle" will always work.


So when the use of a language or product is prolific, such as with LaTeX or Java, then using the name is enough to define what you do.

"What do you do?"

"I do Oracle."

If the use of Isabelle was prolific, then the use of "Isabelle/HOL" would set the context. But Isabelle/HOL is relatively unknown in the programming world, and it wouldn't solve my need for a word like "programmer". Or maybe it would.

"What do you do?"

"I write HOL source."

But it's not prolific. So to say, "I write HOL source", is to invite the question, "Oh, that sounds interesting. But what is that exactly?"

Instead of,

"What do you do?"

"I'm a programmer."

"Oh." (Their eyes shift around, looking for someone else to talk to. That's good. You didn't feel like talking about it either.)


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