Re: [isabelle] automatically grade Isabelle homework?



On 07/11/2016 10:43 AM, Lars Hupel wrote:
> the safe mode also prevents the student from adding ML code that allows
> them to implement a bad oracle, i.e. their own "sorry", right? Will
> there be another way of avoiding that, once the safe mode is gone?
There are more ways to cheat than that, e.g. with "axiomatization" or
introducing custom or changing existing input/output syntax. However, ML
oracles can be easily detected using "Thm.peek_status" (the "oracle"
field is set to "true").

This is not reliable either. You can hide usage of an oracle in the instance proof when you instantiate a type class. For example, create a type class that assumes False and use sorry in the instance proof.

Probably the most reliable way that we can amend this is to remove the axiomatic type classes from the kernel.

Bests,
Ondrej




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