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

Thanks a lot!


Le 30/04/12 14:22, Johannes Hölzl a écrit :
Hi Thomas,

I added a link to your course material in the Community Wiki:

  - Johannes

Am Donnerstag, den 26.04.2012, 16:14 +0200 schrieb Thomas Genet:
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.

Good points:

++ 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
function) was
++ 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 more
      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
    equation, e.g.:

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 as a
    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.

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.