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



On Fri, 18 Sep 2015, Andrei Popescu wrote:

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.

OK, so I take the pulished paper as is, taken from http://www4.in.tum.de/~kuncar/documents/kuncar-popescu-itp2015.pdf

In the third round of looking at it, I have now started to read the technical part and have already learned many interesting things. I will comment (and criticize) more later, when the big picture has evolved a bit further.


I need to appeal again to the professional routine of the Isabelle development and release process. Users will have true reasons to get worried, when non-trivial changes to core system components and their very foundations can be pushed-in just by making a lot of noise in public.

I've not been at the ITP talk, but I can imagine how it went, just by extrapolating the style and manner of some paragraphs in the paper.


You may remember yourself that the initial idea of BNF (co)datatypes was expected to be implemented in one year, or so. Ultimately it required many years, and several wizards to finish the job. Behind the scenes we even had to get David Matthews involved, to extend the playground of the ML platform. I also had to make "dangerous experiments" again -- as you call it in the paper -- in order to have it all go through smoothly.

Adapting the ideas presented in the presented paper in the proper way for Isabelle will not take as long as BNF datatypes, but it is not immediate.

It could have been finished already, if we did not have serious meta-problems that are still ignored by most participants of the debate. This is why I spend so much time here, instead of looking through ML sources.


	Makarius




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