Re: [isabelle] Isabelle Foundation & Certification

On Wed, 16 Sep 2015, Larry Paulson wrote:

It would be interesting to find out how these problems were identified: whether they were looked for out of curiosity, or whether on the other hand they manifested themselves in the course of an actual proof.

This is an important point that is rarely explored systematically. From my own experience in the past 10-15 years:

  * "synthetic problems" of the first kind are encountered about 2 times
    per year; typical changes are ff75ed08b3fb (2001) or ccbf9379e355

  * "practical problems", i.e. those encountered in actual applications
    are encountered every 2-3 years

What happens all the time are misunderstandings by users about concrete syntax or concrete syntax that is actually wrong. Nobody is worried about that as a custom.


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