Re: [isabelle] Isabelle Foundation & Certification (answer to Makarius)



Hi Makarius, 

First, I thank you very much for looking into this. I have a conference tutorial to prepare for this Sunday, and this is why I will be rather brief in my reply. Next week I'll address 
the points you are raising in much greater detail. 

Second, if you can, please ignore that reference to the technical report -- it is indeed a lingering reference, which we unfortunately forgot to remove. At the preparation of the camera-ready, we managed to 
include sufficient technical details in the paper, especially since we received an extra page. So now the paper essentially includes that report. I am here to offer any missing technical details, should you 
request any -- but if you read the paper in good faith, it is likely you will not even need additional explanations.  

Third, I kindly ask you that, during our discussion about this, you respect my different opinion here, which can be summarized as follows: 

BEGIN opinion 

Even though Isabelle/HOL is implemented on top of a logical framework, we can conceptually speak about its structure as: 

(A) a logic L, consisting of axioms and rules of deduction

(B) the logic L augmented with a definitional mechanism (namely, type and constant definitions) -- let me call it L_D

The current situation with Isabelle/HOL is the following: Even though L is consistent (in that it cannot prove False), L_D is inconsistent (in that it can prove False).

END opinion 

Even though, as the developer of the Isabelle *software* , you believe the situation is much more complex, I kindly ask you to make an effort and understand this point of view. 
The purpose of any logical framework (including Isabelle/Pure and Edinburgh LF) is to facilitate the implementation of a logic, not to intrude with the logic. I am sure that the implementation of 
Isabelle/HOL inside Isabelle/Pure does a good job at achieving this. I am saying this as a fairly experienced user of Isabelle/HOL.  

The development from our paper works with the logics L and L_D assumed above. Again, if you read the paper in good faith, you will be able to understand what is being proved there and perhaps 
convince yourself that the proposed change to the system will at least achieve the following goal: prevent certain ways of proving False which is particularly disturbing to many many users. 

Finally, I have a possibly strange request: Please do not trust your judgement *alone*, because you (like anybody else) may be wrong, and may not realize it because of the way you look at things. 
There must be someone (at least one person) on this mailing list whose judgement you trust. Please ask that person for a second opinion about: (1) the actual problem discussed here and (2) the solution we propose in the paper. 
If possible, please also make the name of that person public.  

All the best and talk to you again soon, 
   Andrei 


---------------------------------------------------------------------------


Please note that Middlesex University's preferred way of receiving all correspondence is via email in line with our Environmental Policy. All incoming post to Middlesex University is opened and scanned by our digital document handler, CDS, and then emailed to the recipient.

If you do not want your correspondence to Middlesex University processed in this way please email the recipient directly. Parcels, couriered items and recorded delivery items will not be opened or scanned by CDS.  There are items which are "exceptions" which will be opened by CDS but will not be scanned a full list of these can be obtained by contacting the University.





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