Email Gateway (Aug 18 2022 at 19:24): Email Gateway (Aug 18 2022 at 19:24):From: Makarius <makarius@sketis.net>
In preparation for the coming relase, I've gone through the sledgehammer
and nitpick connectivety again a few days ago, and refined it a little
bit. There were some minor instabilities and potential race conditions
wrt. editor buffer content, but no fundamental problems as far as I could
see.
Public announcements for Isabelle2012 release candidates will come next
week on this mailing list, so you can try again and report pending
problems.
Makarius
Email Gateway (Aug 18 2022 at 19:24):From: Makarius <makarius@sketis.net>
I have looked a bit through the course material. What is always
interesting is to see what users get as "survival kit" -- it provides some
hints what are the fine points that can be improved in the system itself,
for people getting exposed to it the first time.
The introduction of sledgehammer to "Solve theorems in the Cloud" is also
nice. Someone told me he always explains the algebraic law of
associativity in terms of the Google Map-Reduce framework :-)
You mention OCaml occasionally in passing, as if it could be assumed as
background of French students. Is this the case? I am giving a 2-day
Isabelle/HOL tutorial in 2 weeks at Paris Sud, so it would be good to know
if OCaml can be taken for granted.
What I have already learned is that Coq can not be taken for granted
here in France, even though international conferences on theorem proving
sometimes give a different impression.
Makarius
Email Gateway (Aug 18 2022 at 19:24):From: Makarius <makarius@sketis.net>
Just for the record, this is the website:
http://www.lri.fr/~wenzel/Isabelle_Orsay_2012
If anybody in the area wants to participate, or knows someone who might be
interested, feel free to contact me via email. (Although we are already
close to being overbooked.)
Makarius
Email Gateway (Aug 18 2022 at 19:25):From: Patrick Michel <uni@pbmichel.de>
Hi!
I have looked a bit through the course material. What is always interesting is to see what users get as "survival kit" -- it provides some hints what are the fine points that can be improved in the system itself, for people getting exposed to it the first time.
I'd like to chime in on that by noting that we do a course on "Specification and Verification with Higher-Order Logic" in Isabelle/HOL as a Master's course.
Last year we set up a wiki (https://svhol.pbmichel.de) for the students, so we could dump in some knowledge about Isabelle/HOL, the proof general, HOL theory and general emacs.
It was also mainly designed for the students to contribute; the wiki is world-editable. Feel free to contribute :-)
Maybe the site is of some interested to one or the other. Regarding the above quote I'd say our FAQ - Ask Questions section might be of interest :)
Patrick Michel
Software Technology Group
University of Kaiserslautern
Email Gateway (Aug 18 2022 at 19:26):From: Thomas Genet <thomas.genet@irisa.fr>
Le 28/04/12 15:39, Makarius a écrit :
You mention OCaml occasionally in passing, as if it could be assumed as
background of French students. Is this the case? I am giving a 2-day
Isabelle/HOL tutorial in 2 weeks at Paris Sud, so it would be good to
know if OCaml can be taken for granted.
For french students, I would say yes...
What I have already learned is that Coq can not be taken for granted
here in France, even though international conferences on theorem proving
sometimes give a different impression.
Yes, it is true. The overall knowledge of Coq highly depends on the
university where you come from. You are very much likely to be exposed
in "Research" Masters (you probably know this distinction we have in
France now that you are at LRI :-) ... The course that I gave was
designed for "Professional" Masters... which explains that it does not
put the stress on proofs tactics and so on.
Best regards,
Thomas
Email Gateway (Aug 18 2022 at 19:28):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Thomas,
I added a link to your course material in the Community Wiki:
https://isabelle.in.tum.de/community/Course_Material
Email Gateway (Aug 18 2022 at 19:28):From: Thomas Genet <thomas.genet@irisa.fr>
Thanks a lot!
Thomas
Email Gateway (Aug 18 2022 at 19:37):From: Thomas Genet <thomas.genet@irisa.fr>
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?
Best Regards,
Thomas
Email Gateway (Aug 18 2022 at 19:37):From: Makarius <makarius@sketis.net>
This is one of these scoping errors that then lead to a conflict with the
type constraints imposed by already defined entities, and are thus
discovered indirectly. The type checking phase could be a bit more
ambitious to maintain precise position information and report that (which
is technically not so easy and might require one or two more release
cycles to materialize).
But the actual scoping is already represented quite nicely in current
Isabelle2011-1 right now, if you use Isabelle/jEdit and rely in its
"Haribo effect". This means the sources are painted in funny colors
according to the role of identifiers. The Prover IDE also has the magic
CONTROL (or COMMAND) key, which asks the system to explain the formal
status of some piece of source.
So the above "id" would have come out black (constant) instead of the
expected blue (free variable), and its tooltip would have said "constant
Fun.id", with a hyperlink to jump to its definition in main HOL. So
students would have to spend less energy divinating the meaning of the
text themselves.
Makarius
Email Gateway (Aug 18 2022 at 19:37):From: Lukas Bulwahn <bulwahn@in.tum.de>
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.
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.
Lukas
Email Gateway (Aug 18 2022 at 19:37):From: Thomas Genet <thomas.genet@irisa.fr>
Le 26/04/12 17:21, Makarius a écrit :
This is one of these scoping errors that then lead to a conflict with
the type constraints imposed by already defined entities, and are thus
discovered indirectly. The type checking phase could be a bit more
ambitious to maintain precise position information and report that
(which is technically not so easy and might require one or two more
release cycles to materialize).
aouch... it sounds that it is unlikely to be present in Isabelle/HOL for
next january, the next time I will give the lecture :-)
But the actual scoping is already represented quite nicely in current
Isabelle2011-1 right now, if you use Isabelle/jEdit and rely in its
"Haribo effect". This means the sources are painted in funny colors
according to the role of identifiers. The Prover IDE also has the magic
CONTROL (or COMMAND) key, which asks the system to explain the formal
status of some piece of source.So the above "id" would have come out black (constant) instead of the
expected blue (free variable), and its tooltip would have said "constant
Fun.id", with a hyperlink to jump to its definition in main HOL. So
students would have to spend less energy divinating the meaning of the
text themselves.
Ok I'll try this... In fact, I was nearly ready to use jEdit for the
labs but I found that jEdit was often getting stuck when using nitpick
and quickcheck, and since my labs strongly rely on those two tools it
was a problem.
However, I am convinced that students would love switching to jEdit
because they are really not comfortable with emacs :-)
Best regards,
Thomas
Email Gateway (Aug 18 2022 at 19:38):From: Thomas Genet <thomas.genet@irisa.fr>
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?
Yes!
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
Email Gateway (Aug 18 2022 at 19:38):From: Thomas Genet <thomas.genet@irisa.fr>
Dear Makarius,
I just played a bit with both the "Haribo effect" and the "magic"
COMMAND key that are both very nice functionnalities! I will consider
switching to jEdit. Can you tell me if the behavior of jEdit with
nitpick has been improved?
Thanks in advance,
Thomas
Email Gateway (Aug 18 2022 at 19:49):From: "Charlie (Cheolgi) Kim" <cheolgi@gmail.com>
Thank you for the good resource.
Indeed, I am using the material to teach myself Isabelle. The material is
awesome.
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
errors.
Can anybody guide me?
Thank you.
Best,
Charlie Kim
Email Gateway (Aug 18 2022 at 19:49):From: Lawrence Paulson <lp15@cam.ac.uk>
Probably you just need parentheses: (% x. f x) = (% y. f y)
The scope of a variable-binding operator is unlimited in both directions (left and right). This is a peculiarity of Isabelle's parser.
Larry Paulson
Last updated: Apr 26 2024 at 12:28 UTC