[TYPES] SASyLF proof assistant: teaching experience

[Jonathan Aldrich]

If you're planning to teach a programming language or logic foundations 
course and are thinking about using a proof assistant, you might 
consider SASyLF.  SASyLF (Second-order Abstract Syntax Logical 
Framework) is an LF-based proof assistant that the same logical 
foundation and many of the same advantages as Twelf (in particular, 
variable binding is "built in").  However, it uses a syntax very close 
to that used for proofs on paper, giving the tool a much gentler 
learning curve--and much better error messages--than many alternatives.

In Fall 2008, John Boyland at UWM and Todd Millstein at UCLA used SASyLF 
for their type theory courses.  Sample homeworks are available at 
Boyland's course page: they include proof exercises from Pierce's book, 
which students did in SASyLF, all the way up to advanced chapters such 
as 20, 22, 23, and 30:

http://www.cs.uwm.edu/classes/cs732/index-fa08.html

Experience with SASyLF from the courses was very positive.  In 
particular, feedback from a student post-survey included (Likert scale 
1-5, 5 is strongly agree):

  * Would like to use SASyLF in another PL course: 4.2
  * Able to learn SASyLF quickly: 3.8
  * SASyLF improved my ability to prove theorems, even on paper: 4.0
  * SASyLF enabled me to accomplish tasks more quickly: 3.3

More information, the SASyLF command-line proof checker, and a very 
simple Eclipse-based IDE, are available at:

http://www.sasylf.org/


SASyLF is not ideal for everything.  It shares many of the disadvantages 
of Twelf--e.g. things like sets are neither built-in nor available as 
generic libraries, and it supports only forall-exists theorems (good 
enough for many PL theorems including typical type soundness theorems 
but not enough for e.g. logical relations).  SASyLF is also more verbose 
than Twelf (probably a good thing for teaching, but perhaps not so good 
for research-scale proofs) and since it is second-order it does not 
support some higher-order encodings that Twelf does.  But we 
nevertheless believe it can be a valuable tool in many classrooms!

Contact me if you have any questions.

Jonathan Aldrich