I have no disagreement with what FL writes. However, saying "TLA+ is
hard, but it's good for you" will needlessly scare away students. Every
user of a non-trivial language just uses a subset. I use a subset of
English. Engineers can learn a subset of TLA+ that allows them
to use it in their work in two or three weeks.
I think it's usually better to start students using PlusCal rather
than TLA+. However, they should know enough TLA+ to understand the
TLA+ translation of their PlusCal algorithms. Computer people tend to
believe that languages have magical powers. All you need to solve a
problem is to find the right language. Believing in magic is not
conducive to proper thinking. Students need to learn to think of
programs as specifying an initial states and next-state relations.
they use describe a program in terms of an initial predicate and
next-state relation.
Since Daniel is teaching about formal logic and program verification,
what is "usually better" may be best for his purposes.
Leslie
On Monday, December 16, 2013 9:04:51 AM UTC-8, Daniel Leivant wrote:
I plan to incorporate next semester an introduction to TLA (and
temporal logic) into a graduate introductory course on formal logic
and program verification.
If anyone has any ideas, material, pointers, or experience to share,
that would be tremendously helpful and greatly appreciated.
Thanks much in advance and best wishes - Daniel
Daniel Leivant
Professor of computer science
and adjunct professor of mathematics
Indiana University Bloomington