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



Hi Thomas,

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

  https://isabelle.in.tum.de/community/Course_Material

 - 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:
> 
> http://www.irisa.fr/celtique/genet/ACF/
> 
> 
> 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
> 







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