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$
6
  • 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$ May 8, 2012 at 18:26
  • 2
    $\begingroup$ Eh, tags are free. Unless you object, I'll add it. $\endgroup$ May 8, 2012 at 19:00
  • 1
    $\begingroup$ Tags help categorize questions. A more general tag would be more useful. Maybe programming-languages $\endgroup$ May 8, 2012 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$ May 8, 2012 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, 2012 at 22:28

1 Answer 1

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$
15
  • $\begingroup$ I think there are proof systems for actor languages. These might provide some sort of ground zero. $\endgroup$ May 8, 2012 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$ May 8, 2012 at 21:22
  • 1
    $\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, 2012 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, 2012 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$ May 13, 2012 at 12:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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