Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy


I was going to let your email be the end, a decision which actually resulted in me culling out every point I thought about making, except for trying to make a point with your transportation analogy.

To summarize the point to begin with, so you don't have to actually read the analogy, it's just a variation of my past "Isabelle is awesome" statements.

So Isabelle/HOL is a Boeing airplane, though a special model that's configurable, and Haskell is a Ford car.

In regards to transportation, it appears not to make sense for a person to make anything but the broadest of generalizations when comparing the two.

That's because, Isabelle, being a Boeing airplane, is certainly a means of transportation, but the maintenance and fuel costs are extraordinary, and so on the surface, to point out that Haskell, a Ford car, hasn't implemented certain theoretical, engineering concepts when Isabelle has, can appear to be dumb, especially, because practically speaking, as far as transportation the advanced features are of no use.

However, the proper context is my use of the special, configurable Boeing airplane. It happens to be that I have almost no interest in traveling, I only care to theorize about traveling, in particular, theorizing about air travel.

At this time, I don't have the money to even have the Boeing started up, but then again, at this point, I only have a need to look at the Boeing, and take a few measurements for certain parts that aren't completely documented.

Now, I would hope that in several years, I'm doing something more than what has already been done in regards to theorizing about air travel, to the point to where I have a need to do more than just look at the airplane, but in two years time, manufacturing costs being what they are, there's some chance it will be affordable for me to pay some per minute charge to reconfigure the special Boeing, where simply reconfiguring it should answer some question I'll have.

So forth and so on. As times passes, what was once not affordable becomes affordable, in regards to testing my theories. The upside is that I may never have to resort to buying a Ford car, which is accessible to the masses, but still costs a lot of money, and is a waste if I don't have to do it.

And there's the possibility, if I can keep postponing the need for a Ford car, that at some point, the configurable Boeing has ceased to be leading edge technology, for near exclusive use by academics and researchers, but the costs have dropped so much that it has become commodity technology, and things have evolved for me to the where I now have a need to travel, but not simply on the ground, like with the Ford car, but in the air.

Do the designers intend for a person like me to use the Boeing in this way? Probably not. Most likely, the configurable Boeing is meant as an ends to a mean for professionals who work in the aerospace industry.

But instead of of using the configurable Boeing as an ends to a means, I use it as an ends in itself, and because it can be used like that, it's awesome.

Well, because I have no desire to ever work outside the realm of the configurable Boeing, certain vocabulary doesn't fit my use of the Boeing as good as it fits the designers use, but that idea is not to be pursued here.


On 5/22/2013 9:27 AM, Lawrence Paulson wrote:
You can call anything anything, but you are only complicating things for yourself. To my mind, asking why Isabelle/HOL has equivalence classes when Haskell doesn't and they are both programming languages is a bit like asking why a Boeing can fly and a Ford cannot when they are both cars.

Perhaps the term you are looking for is "formal language". Programming languages are formal, and higher-order logic is also a formal language. Just as Boeings and Fords are both vehicles.

Larry Paulson

On 22 May 2013, at 15:02, Gottfried Barrow<gottfried.barrow at>  wrote:

On 5/22/2013 8:26 AM, Lawrence Paulson wrote:
Coq and Isabelle/HOL are proof assistants, not programming languages. I can't imagine what gave you that idea. In Coq and Isabelle/HOL you write specifications, not code.

Larry Paulson

My general rule is to never use emoticons, but rules have their exceptions.

You gave me that idea :). As to acronyms such as "lol", even under these circumstances, they're still unacceptable.

This is the specific email:

This will contain the thread:

I was just starting to decide that under certain contexts, I could refer to Isabelle/HOL as a programming language, because it's just a lot easier to use that phrase sometimes, whereas, according to your specific clarification in the email linked to above, Isabelle/Pure and Isabelle/Isar are never to be called programming languages, so I try to use "proof language" or "source language" when referring to them, even when I know others might not get my point.

One of my other recent emails to the list spawned some private chatter in which I referred to HOL as a programming language, which resulted in a similar response to yours,  which paraphrased would be, "What is this programming language you're talking about in reference to HOL?"

That's why I had easy access to the links above, because I thought I had the perfect, authoritative reference to explain that Isabelle/HOL is a programming language, where Pure and Isar aren't.

In an attempt to use safe, correct vocabulary, I've resorted to using "coding language" when trying to refer to the whole Isabelle family of languages. At some point, there's a need for phrases, like, "I'm programming with Isabelle/HOL", or, "I'm coding with Isabelle". Like I say, "coding" has become my word of choice to replace "programming".

Anyway, I'm happy to try and use the official vocabulary correctly. There are a ton of interwined languages with Isabelle, so I give up and get lazy sometimes, and just say "programming language".

As to Coq, it seems to me if I can call Isabelle/HOL a programming language, then I can call Coq a programming language. That's just an aside. I'd be happy to use any official Coq vocabulary to use to refer to Coq.

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