[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] C0 and TLAPLUS


> 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.