5
$\begingroup$

Well, today I just got my 15 minutes of fame, but now I think I am wrong on the point about formal proofs on Erlang systems. The discussion on news.ycombinator.com suggests that Erlang code may or may not lend itself so well to formal reasoning (and it's certainly not pure a pure functional language), although a bit of google-fu turns up a fair number of peer reviewed articles on formal proofs on Erlang systems.

I'd like to get this right. Can somebody here give a decent, in-depth explanation of the ins and outs of formal proofs on Erlang systems?

$\endgroup$
  • 2
    $\begingroup$ I don't think we need an erlang tag. Erlang does not often come up in the context of theoretical computer science. $\endgroup$ – Dave Clarke May 8 '12 at 18:26
  • 2
    $\begingroup$ Eh, tags are free. Unless you object, I'll add it. $\endgroup$ – Neel Krishnaswami May 8 '12 at 19:00
  • 1
    $\begingroup$ Tags help categorize questions. A more general tag would be more useful. Maybe programming-languages $\endgroup$ – Dave Clarke May 8 '12 at 19:34
  • 1
    $\begingroup$ @DaveClarke, Maybe a tag "actor-model" would be appropriate since proof techniques for those systems would be relevant to this question and more widely. $\endgroup$ – Mike Samuel May 8 '12 at 22:00
  • 1
    $\begingroup$ What is the basis for claiming that Erlang is good for formal proofs? Has somebody written denotational semantics for it? Or a programming logic? Is it based on a well-understood theoretical framework? $\endgroup$ – Uday Reddy May 9 '12 at 22:28
5
$\begingroup$

Erlang is a concurrent, higher-order programming language. To a decent approximation, this covers everything difficult about program verification.

When a language is higher-order, the control structure of the program is not evident from the source code, since code are values, and so the control structure depends on the data flow in the program. When a language is concurrent, this means you have to reason about interference -- the possibility that multiple processes are trying to act on the same data at once. As a result, you have to think through all the possible interleavings of thread executions.

Erlang is a reasonably clean language design, so it doesn't layer many accidental difficulties on top of these two. But those two capabilities ensure that the essential difficulty is not easy.

In fact, it's fair to say that the general problem of how to verify concurrent higher-order programs is still open -- proofs still tend to be tour-de-force efforts, rather than a systematic application of a methodology. We're a lot closer than we were five or ten years ago, though.

$\endgroup$
  • $\begingroup$ I think there are proof systems for actor languages. These might provide some sort of ground zero. $\endgroup$ – Dave Clarke May 8 '12 at 21:14
  • $\begingroup$ A little google-fu turns up plenty of peer-reviewed publications about proofs and reasoning about Erlang systems, and I was given to understand that a lot of the code base for the AXD301 had been subjected to formal proofs of some description. $\endgroup$ – ConcernedOfTunbridgeWells May 8 '12 at 21:22
  • $\begingroup$ I am not convinced that speaking in generalities is enough to make an assessment. Erlang seems to be quite a specialized language design. So, the general statements may or may not apply. $\endgroup$ – Uday Reddy May 9 '12 at 22:24
  • $\begingroup$ You can find formal proofs about and mechanised semantics for subsets of C, C++ and Java as well. $\endgroup$ – Vijay D May 10 '12 at 8:00
  • 2
    $\begingroup$ @MartinBerger: Basically, I want intuitively simple programs to have simple proofs. However, I don't know how to formalize this criterion, and I don't understand its relation to relative completeness. For example, if you drop the magic wand from separation logic, the result is horrible (i.e., you can't state weakest preconditions anymore), but it hardly affects the practical usability of the logic! But since relative completeness is parameterized by the entailment relation, it's (by design) fairly insenstive to variations in the assertion logic. $\endgroup$ – Neel Krishnaswami May 13 '12 at 12:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.