Re: [isabelle] A course based on Isabelle/HOL and some feedback...
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.
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?
Further Isabelle tools adressing the problems of the remaining 50% might
be interesting to consider in the future.
On 04/26/2012 04:14 PM, Thomas Genet wrote:
Dear all Isabelle users,
as promised to Tobias and Jasmin here is some feedback and teaching
material for a course that I gave this year on Formal Analysis and
Design to students in a first year of Master in computer science.
This course was designed for our "professional" master students i.e.
that will end up developpers and not for "research" master students
that will end up in PhD. Thus, I focused on functional programming
(Isabelle/HOL and Scala), first order logic (for defining program
properties) and on counterexample finding (rather than on proof). The
final objective is to run Java+Scala programs with verified blocks,
i.e. whose formally defined properties have been checked on the
Isabelle theory using counterexample finders.
The page of this course is here:
With regards to the experience the students had with Isabelle/HOL here
are some comments. I already sent them to Tobias and Jasmin but Jasmin
advised me to send them on the mailing list.
++ Though 80% of the students were initially allergic to functional
programming, in the end they are almost all convinced that it is
a convenient formalism to define and prove programs.
+++ Students allergic to logic ended up in writing relevant lemmas
(this point deserves three +, because it was my main objective)
++ Most of the students allergic to logic ended up in being convinced
that writing a lemma may replace writing a test
++ Some of the students ended up in being convinced that writing a
lemma may replace writing a thousand tests :-)
+++ Counterexample generation makes it possible for the students to
quickly figure out which of their definition (the lemma or the
++ The code export to Scala was very much appreciated ... it makes the
formal verification of functional program sounding useful to
++ Counterexamples found by nitpick and quickcheck permitted to debug
rather complex functions (see practicals in the following). They
were intensively used by students.
Bad points and suggested improvements:
--- Function parser and error messages are sometimes very poor... which
makes the debugging very difficult... especially for functions of
than 10 lines the error message just mention that there is an error
somewhere... well, thanks :-) At least, a line number for the error
would be much appreciated.
-- It is a bad idea to use a variable name like id in a function
fun f:: "nat => nat"
OK, the error message says:
*** Type error in application: incompatible operand type
*** Operator: f :: nat => nat
*** Operand: id :: ??'a => ??'a
and a (careful) student may understand that 'id' is already defined
function etc... however this is far more difficult to find when the
function has 10 complex equations. What surprises me is that the
left-hand side of the equation f(id) does not respect the restrictions
for "fun" declarations and that it should be rejected anyway (with a
more explicit error message). Am I right?
- Indentation of function equations (inside the "...") is simply
horrible (in emacs) as soon as you have several if and case
constructions, or I did not understand it.
This archive was generated by a fusion of
Pipermail (Mailman edition) and