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
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and