> I had a quick look at C0 and it looks definitely easier to verify than
> pure C (e.g. there is no typecasting). If I understand correctly, the
> difference to Pluscal is that C0 has explicit memory management, an I/O
> library and contracts.
There is no memory management, malloc, free and so on. It is obvious that
Pfenning has removed all the C features that make the things harder to be proved.
His goal is to teach algorithms and how to prove prove them. I think he has done
a very interesting work
> I'm not sure what role you envision for C0 in combination to TLA
I agree with Leslie Lamport's philosophy that programming languages
is not the right level to design an algorithm.
> the verification process - in particular you need to prove that memory
> management is correct
There is no memory management.
> Insofar I'd prefer to teach a purely functional language like Haskell,
> which is closer to logic (e.g. that it doesn't have assignment or the
> way list comprehensions resemble mathematical set comprehensions) and
> better suited to reasoning on parallelism.
I think you can't avoid teaching one imperative language. At least
because it gives you a feel of how the machine works. It is not the case
of functional languages.
And I wonder if TLAPLUS is well suited to functional programming.
I know that Leslie says that it is possible. I'm dubious.
> At least I have the feeling
> that the gap between C0 and Pluscal is esier to understand than that
> between Pluscal and TLA.
Yes that's sure.
--
FL