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

Thank you for the good resource.

Indeed, I am using the material to teach myself Isabelle. The material is
However, I found that myself cannot solve an exercise:
Prove a property of the %-calculus: % x. f x = % y. f y
which looks trivial, but whatever I try to make a lemma, they make syntax

Can anybody guide me?

Thank you.


Charlie Kim

On Thu, Apr 26, 2012 at 11:14 PM, Thomas Genet <thomas.genet at>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.
> 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
>    false.
> ++ The code export to Scala was very much appreciated ... it makes the
>   formal verification of functional program sounding useful to developpers!
> ++ 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"
> where
> "f(id)=id"
>  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
> --
> Thomas Genet
> Campus de Beaulieu, 35042 Rennes cedex, France
> Tél: +33 (0) 2 99 84 73 44 E-mail: genet at
>**genet <>

Charlie (Cheolgi) Kim
Visiting Research Scientist,
Real-Time System Integration Group,
University of Illinois

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