2016-07-09 09:04:16 UTC
I wonder about the feasibility of the following.
Perhaps something similar has already been done.
I want to automatically check solutions for homework assignments.
The problem statement could be a text with some "sorry",
and the student has to replace these with actual proofs,
and is forbidden to change anything else.
I am already doing this for Haskell homework -
students have to replace "undefined",
resulting code is type-checked and then small/quick-checked.
See URL at end of this mail for implementation.
1. what is the best way to pattern-match
student's Isabelle code against problem statement?
For Haskell, I actually compare abstract syntax trees.
2. how safe is it to run Isabelle? - For Haskell,
anything dangerous would be in IO, which is prohibited
by putting type annotations in the problem statement
(which the student cannot change).
And "unsafePerformIO" is prohibited because it would need
some "import" statement - which again would not survive
the pattern matching. So, the worst that can happen
is that student's code runs forever,
and for that I just limit execution time (to a few seconds).
Is there any way to sneak an IO action into a proof?
3.1 How would I run Isabelle? Of course I don't want the GUI.
3.2 Can I avoid putting student's submission in a file,
and pipe it instead?
3.3 How would I detect that Isabelle actually verified the proof?
Ideally, just by checking the return code?
Any input appreciated.
NB: I once saw an (unrelated) project
that used "maxima" to check elementary algebra homework,
and this had serious security holes -
you could easily do IO because there is no static checking.