Re: [isabelle] A course based on Isabelle/HOL and some feedback...

Dear all,

Le 26/04/12 17:23, Lukas Bulwahn a écrit :
Hello Thomas,

I am impressed that simply writing and validating specifications with
Nitpick and Quickcheck could improve the correctness of the
implementations by 45%.
As you write, only 5% of the students got the right solution without
Isabelle in the beginning of the course, and 50% students ended up with
the correct program within 2 hours using Isabelle at midterm.

If you look at the predicate I was asking for it was not that complex to write in Isabelle/HOL (I realize that the subject of the lab is in french... sorry, I can translate it in french if you want to try)... I mean it is not straightforward but it only consists of 2 recursive functions... However, I think that coming up with the good solution at the first try is difficult.

Can you say more why 45% succeeded at midterm? Was it simply the
application of our counterexample generators and forcing students to
think about their specification?


Why did the remaining 50% fail? Did they never get the specifications
right? Or did Quickcheck and Nitpick fail to find counterexamples?

No they had a hard time finding the good algorithmic idea and they are also beginners in functional programming... it is thus hard for them in 2 hours.

Further Isabelle tools adressing the problems of the remaining 50% might
be interesting to consider in the future.

except a tool automatically writing the functions from the specification ... I do not see how to help them :-) They were only lacking practice of functional programming. At the end of the course, they were more comfortable with this.

Best regards,

Thomas Genet
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet at

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