C0 and TLAPLUS

I think that Franck Pfenning C0

> http://c0.typesafety.net/

> http://www.cs.cmu.edu/~fp/papers/pic11.pdf

> http://www.cs.cmu.edu/~fp/

and concurrent C0 (but it doesn't see that it can be already downloaded)

> http://www.cs.cmu.edu/~fp/papers/cc016.pdf

is worth being used with TLAPLUS.

C0 is a simplified version of C. You don't have the burden of the ununderstandable standard of C and
you benefit however of a language that looks like C, has pointers and so on. It is so close to C that the
bridge between the two languages is easily crossed. And you also have a contract language. Then it
can be used rigorously.

It is clear that it is THE language that can be used to teach imperative languages.

It can be used with PLUSCAL. I think the two interface well. You teach C0 first then you teach
PLUSCAL. And you show how to combine both. How to design your program with PLUSCAL,
animate it with TLC, prove it with TLAPS and then translate it into C0. You can also show
how to translate the TLAPLUS ASSUME into C0 contract.

That way you have a complete combined envrionment, PLUSCAL for the design and C0 for
the implementation. With the rigor guaranteed at every level.

--
FL