C0 and TLAPLUS

[fl]

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

[Martin]

Hello,

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.

I'm not sure what role you envision for C0 in combination to TLA though
- it might be easier to teach verification when you already know about
assertions and loop invariants. But the other features of C0 complicate
the verification process - in particular you need to prove that memory
management is correct and are bound to C-like data-structures like
null-terminated strings. I believe they distract a student from
reasoning on the actual algorithm and put the focus on the book-keeping
a C like language enforces.

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. At least I have the feeling
that the gap between C0 and Pluscal is esier to understand than that
between Pluscal and TLA.

What I would find interesting though would be code-generation from a
reasonable subset of Pluscal (full Pluscal allows arbitrary TLA
expressions like CHOOSE x : ~(x \in Nat) - which shouldn't be
translated to an iteration on the whole set of natural numbers).

cheers, Martin

> --
> You received this message because you are subscribed to the Google
> Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to tlaplus+u...@googlegroups.com
> <mailto:tlaplus+u...@googlegroups.com>.
> To post to this group, send email to tla...@googlegroups.com
> <mailto:tla...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[fl]

 

> 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

[Martin]

On 09/06/2016 11:42 AM, 'fl' via tlaplus wrote:
>
>
>> 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

It seems I scanned the pages too quickly -- there exists an alloc_array
for arrays and alloc for pointers (see page 9 of the language
reference), but there is indeed no free (but garbage collection). This
puts C0 definitely closer to Java, but the direction in which C1 shows
that one language goal is definitely to lead a student to understand the
hard parts of C.

But then C0 addresses are still a data-type which can be compared (and
in C1 also computed with) which means that for reasoning over data, we
must take the memory address into account. Apart from understanding the
algorithm better, this explicit representation of memory still presents
a challenge to verification. I'm pretty sure can already see a
difference when you introduce a reference/dereference function (from
Datatype -> Address \subset Nat) in TLA and compare the performance of
TLC when you model sorting via a Sequence and explicit memory.

You can also see the added load on a model checker / theorem prover in
the C-style strings. A correct program needs to ensure 0-termination -
which also introduces the invariant that a string may not contain the
0-character. That's stuff you'd like to abstract from, when you model
messages between actors.

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

I agree - luckily with languages like Scala the paradigms are
converging. Reasoning over Scala is still hard, but it gives programmers
the chance to have some pure building blocks they can work with. My hope
is that the impure parts will become even smaller over time such that
reasoning capabilities on actual code improve.

> And I wonder if TLAPLUS is well suited to functional programming.
> I know that Leslie says that it is possible. I'm dubious.
>

What works similar in functional programming is that pure functional
programming enforces an explicit state (often called an accumulator). A
state update is then a function from old state to new state. That's
exactly what you need to do in logic too.

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

cheers, Martin

[Leslie Lamport]

   And I wonder if TLAPLUS is well suited to functional programming.
   I know that Leslie says that it is possible. I'm dubious.

I can't imagine that I said that, since I know almost nothing about
functional programming.  I know what a mathematical function is--for
example, it is traditionally defined as a set of ordered pairs.  But
programming is about computation and a set of ordered pairs says
nothing about computation.  I gather that in purely functional
programming one actually describes a function (an ordered pair of
states) in a way that suggests how it can be computed.  You can write
functions that way in TLA+, but I don't know if there's any advantage
to doing that rather than writing them in a functional language.  Since
TLA+ allows writing things in ways that don't suggest how they can be
computed in practice, I suspect that it might be good for specifying
the function to be computed by a functional program.  But I have no
practical experience with this.

In general, concurrent programs need to be described in terms of how
they change the state.  I presume that a purely functional language
has no concept of state, so I don't know how people write such
programs in "functional" languages.  Martin seems to suggest that
"functional" languages are used for concurrent programs by specifying
the next-state relation as a set of functions, each specifying a
possible state transition.  This isn't a good way to write
higher-level specifications, which require relations rather than
functions, but it might be fine for writing programs.  In any event, I
have never seen any published description of a concurrent algorithm
that claims to be written "functionally"; all the ones I've seen are
written using non-functional concepts like assignment.  They're usually
written too informally for it to be meaningful to say that they are
using a functional language in the descriptions.

I find Martin's statement

   a purely functional language like Haskell, which is closer to logic

   ...  and better suited to reasoning about parallelism

rather puzzling.  I think what he means is that if you'rer computing a
function, writing it in a functional language makes it easier to see
how parallelism can be used to speed up the computation of the
function.  While of great practical importance, this kind of
parallelism represents a subclass of concurrency (which can be
rigorously defined) that is very simple.  (I believe that Map Reduce
is a language for describing that class of algorithm.)  In particular,
avoiding errors in such parallel algorithms is no more difficult than
avoiding them in sequential algorithms, so it hasn't interested me
very much. 

Leslie
  

[fl]

 

It seems I scanned the pages too quickly -- there exists an alloc_array
for arrays and alloc for pointers (see page 9 of the language
reference), but there is indeed no free (but garbage collection).

The alloc_array returns an array and can be used only once when the variable is declared.
And as you have noticed, there is no free. So we can't call it a memory management. The
same applies to alloc for pointers.

There is no casting, no pointer arithmetic, no memory management. All what can
make the program difficult to prove has been removed.

Nice teaching idea.

--
FL

[fl]

I can't imagine that I said that, since I know almost nothing about
functional programming.

OK a piece of human misunderstanding due to the lack of formality of the human language :)

I'm happy this ambiguity is cleared up. It made me perplexed.

--
FL

[fl]

I'm not sure what role you envision for C0 in combination to TLA

We might think of a sort of TLAPLUS0. We would use TLC and PLUSCAL.

No TLAPS, no temporal logic and no translation of the PLUSCAL  algorithm
into TLAPLUS macros.

The purpose would be to teach that expressing an algorithm using mathematical
concepts: relations, functions, set builder notation is more interesting than a
language to design an algorithm.

Then the transition of TLAPLUS0 to the rest of TLAPLUS would be easy.

--
FL