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



Sorry, a couple of further brief notes: 

>> This proper distinction also explains, why typedefs were not treated in the past, because it is hard to understand them in generic Isabelle/Pure, without an unfriendly takeover of the framework by HOL troups.

It is of course impossible. We have to let the HOL troops in at this point, there is no way around this.  

>> A few more notes on the paper: I actually liked the "Inconsistency Club" versus "Consistency Club", although it is hard to define that boundary. Just a single Boolean value to measure the reliability and robustness of a 
>> proof assistant in black or white is a bit lacking. Apart from shades of grey, such a measure desparately needs more than one dimension.

"Consistency Club" here does not refer to bullet-proof systems, but to formal efforts of partly ensuring consistency (whatever that means :-)  ). In particular, this club does not contain theorem provers, but formal developments.  

All the best, 
  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.