Re: [isabelle] International Olympiad in Isabelle?



On 18/06/18 14:19, Max Haslbeck wrote:
> 
> Simon and I wrote up a few pages documenting the idea:
> http://www21.in.tum.de/~haslbema/documents/provingcontests_draft18.pdf
> 
> We are planning to push this further in future.
> The technical details aside ...

An interesting paper.

Note that "the ML level" no longer exists in Isabelle today. You mean
"Isabelle/ML", which is properly integrated into Isabelle/Isar for more
than 10 years. In the past, end-users were accustomed to the Poly/ML
bootstrap environment, which is still available in "isabelle process"
and "isabelle console" today, but rarely used directly in applications.

Moreover note that the brief discussion about the 'sorry' command vs.
checking oracle tags in thm values is unfounded. Neither the Isabelle
documentation nor the implementation supports that claim.

Concerning the general mental model of a bullet-proof checker that can
run unattended and cannot be abused: I don't believe that Isabelle can
ever deliver that. It was not constructed with that idea in mind: after
decades of following a model of benevolent users that don't shoot
themselves in the foot, it is infeasible to do differently in a posthoc
fashion. You need a different proof checker for that, but I don't know a
suitable system.


	Makarius




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