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



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 gmx.com> 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
> 
> Larry,
> 
> 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:
> 
> http://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/msg00034.html
> 
> This will contain the thread:
> 
> http://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/thread.html
> 
> 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.