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

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

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

<p>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 <em>tour-de-force</em> efforts, rather than a systematic application of a methodology. We're a lot closer than we were five or ten years ago, though.</p>

CC BY-SA 3.0
2012-05-08T21:14:35.907Z
I think there are proof systems for actor languages. These might provide some sort of ground zero.
Dave Clarke
CC BY-SA 3.0
2012-05-08T21:22:02.197Z
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.
ConcernedOfTunbridgeWells
CC BY-SA 3.0
2012-05-09T22:24:23.163Z
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.
Uday Reddy
CC BY-SA 3.0
2012-05-10T08:00:11.877Z
You can find formal proofs about and mechanised semantics for subsets of C, C++ and Java as well.
Vijay D
CC BY-SA 3.0
2012-05-10T11:48:36.143Z
@Neel. What are your criteria for considering a the problem of program logics for a given language solved? I'm asking because I'm tempted to consider the problem solved, as [this
paper](http://www.sussex.ac.uk/Users/mfb21/publications/icalp08/)
presents a very general approach to logics for type-pi-calculi, where the typing discipline is encoded logically by axioms. The logics are complete in the most satisfactory ways (observational and descriptive). Continuted below.
Martin Berger
CC BY-SA 3.0
2012-05-10T11:51:53.520Z
Since most programming languages L, in particular
higher-order concurrent languages, have straightforward encodings into typed pi-calculus, the encoding can be used to push the logic for the typed fragment of the pi-calculus given by L, back to L itself, obtaining a Hoare logic for L.  Continued below.
Martin Berger
CC BY-SA 3.0
2012-05-10T11:52:36.390Z
This paradigm has now been used
multiple times to obtain logics for programming languages that had
been out of reach for other approaches to constructing program logics,
including the first program logic for languages with call/cc [here](http://www.sussex.ac.uk/Users/mfb21/publications/fsen09/),
the first logic for programming languages with ML-style extrudable
local store [here](http://www.sussex.ac.uk/Users/mfb21/publications/fossacs07/index.html) and various distributed progamming languages (not yet published).
Martin Berger
CC BY-SA 3.0
2012-05-13T12:26:17.540Z
@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.
Neel Krishnaswami
CC BY-SA 3.0
2012-05-15T14:40:28.737Z
@Neel What is a good program logic is a highly interesting question that deserves more work, even if it's unlikely that a universally convincing solution can be found any time soon. However I don't think "simple programs should have simple proofs" is achievable, at least not for notions of simplicity that are somehow related to program/formula/proof length. The reason is that it's quite likely that many simple programs will have only long proofs. For example the specification (in a logic for total correctness) of Collatz's function C (with the parameter being free) {True} C {True}. (Ctd.)
Martin Berger
CC BY-SA 3.0
2012-05-15T14:42:17.830Z
The assertion {True} C {True} probably does not have a short proof (assuming the Collatz function always terminates) in any natural logic. 

One option at this point would be to assume an oracle for Peano arithmetic, ZFC or whatever ambient formalisation of mathematics you are using, and look at the remaining proof length. This would 'measure' the contribution the rules and axioms for the programming language make to the complexity of proofs. If we take this point of view, our approach
looks good: (Ctd.)
Martin Berger
CC BY-SA 3.0
2012-05-15T14:46:57.450Z
characteristic formulae can be inferred by induction on
program structure, and if the program to be reasoned about has n constructors, the proof would have length n+1, with the +1 being the oracle invocation. However, this is misleading in that all we are doing in the first n steps is to translate the operational semantics of the program into (the relevant extension of) first-order logic. So we really only shift all the reasoning complexity to the oracle. characteristic formulae can be inferred by induction on program structure, and if the program to be reasoned about has n constructors, (ctd)
Martin Berger
CC BY-SA 3.0
2012-05-15T14:47:24.233Z
the proof would have length n+1, with the +1 being the
oracle invocation. However, this is misleading in that all we are doing in the first n steps is to translate the operational semantics of the program into (the relevant extension of) first-order logic. So we really only shift all the reasoning complexity to the oracle. (Ctd.)
Martin Berger
CC BY-SA 3.0
2012-05-15T14:48:16.090Z
Regarding dropping magic wand from separation logic hardly affecting
practical usability: I don't know much about separation logic, but
could it not be an effect of selection bias: most algorithms verified
in separation logic don't have much sharing going on, so you can
happily make do with just separating conjunction?
Martin Berger
CC BY-SA 3.0
2012-05-24T21:54:51.773Z
@MartinBerger. I think what Neel is saying is that completeness theorems don't satisfy him.  If you can show him some good proofs of programs which are currently tricky to prove, then we could have a more productive discussion.  (Well, I am in the same boat!)
Uday Reddy
CC BY-SA 3.0
2012-05-25T14:59:35.130Z
@UdayReddy. The predicate "currently tricky to prove" is vague. For any programming language, program and predicate that holds of that program, I can come up with a 'logic' where that predicate is trivial to prove. Conversely, for any logic with good universal properties, it's probably easy to come up with programs that are hard to prove, but that's got little to do with the programming language (e.g. diagonalising over the integers to find counterexamples to Fermat's last theorem).
Martin Berger
CC BY-SA 3.0
2012-05-08T20:22:06.550Z
2012-05-08T20:22:06.550Z
Neel Krishnaswami
<p>Well, today I just got my <a href="https://stackoverflow.com/a/243573/15401">15 minutes of fame,</a> but now I think I am wrong on the point about formal proofs on Erlang systems.  The discussion on <a href="http://news.ycombinator.com/item?id=3943556" rel="nofollow noreferrer">news.ycombinator.com</a> 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.</p>

<p>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?  </p>

CC BY-SA 3.0
2012-05-08T17:42:49.503Z
Could someone with enough rep please create an erlang tag and re-tag the question?
ConcernedOfTunbridgeWells
CC BY-SA 3.0
2012-05-08T18:26:38.100Z
I don't think we need an erlang tag. Erlang does not often come up in the context of theoretical computer science.
Dave Clarke
CC BY-SA 3.0
2012-05-08T19:00:40.757Z
Eh, tags are free. Unless you object, I'll add it.
Neel Krishnaswami
CC BY-SA 3.0
2012-05-08T19:34:49.340Z
Tags help categorize questions. A more general tag would be more useful. Maybe [tag:programming-languages]
Dave Clarke
CC BY-SA 3.0
2012-05-08T22:00:12.467Z
@DaveClarke, Maybe a tag "actor-model" would be appropriate since proof techniques for those systems would be relevant to this question and more widely.
Mike Samuel
CC BY-SA 3.0
2012-05-09T22:28:11.643Z
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?
Uday Reddy
<pl.programming-languages><formal-methods>
What are the limitations on formal proofs of Erlang systems?
ConcernedOfTunbridgeWells
# What are the limitations on formal proofs of Erlang systems?

(Asked by: username_0 on 2012-05-08)

Well, today I just got my [15 minutes of fame,](https://stackoverflow.com/a/243573/15401) but now I think I am wrong on the point about formal proofs on Erlang systems. The discussion on [news.ycombinator.com](http://news.ycombinator.com/item?id=3943556) 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?

**Tags:** pl.programming-languages, formal-methods
> **Comments:**
> **username_0**: Could someone with enough rep please create an erlang tag and re-tag the question?  
> **username_1**: I don't think we need an erlang tag. Erlang does not often come up in the context of theoretical computer science.  
> **username_2**: Eh, tags are free. Unless you object, I'll add it.  
> **username_1**: Tags help categorize questions. A more general tag would be more useful. Maybe [tag:programming-languages]  
> **username_3**: @DaveClarke, Maybe a tag "actor-model" would be appropriate since proof techniques for those systems would be relevant to this question and more widely.  
> **username_4**: 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?  

---

## 1 answers

### Answer by username_2 on 2012-05-08. Score: 5

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.

> **Comments:**
> **username_1**: I think there are proof systems for actor languages. These might provide some sort of ground zero.  
> **username_0**: 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.  
> **username_4**: 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.  
> **username_5**: You can find formal proofs about and mechanised semantics for subsets of C, C++ and Java as well.  
> **username_6**: @Neel. What are your criteria for considering a the problem of program logics for a given language solved? I'm asking because I'm tempted to consider the problem solved, as [this paper](http://www.sussex.ac.uk/Users/mfb21/publications/icalp08/) presents a very general approach to logics for type-pi-calculi, where the typing discipline is encoded logically by axioms. The logics are complete in the most satisfactory ways (observational and descriptive). Continuted below.  
> **username_6**: Since most programming languages L, in particular higher-order concurrent languages, have straightforward encodings into typed pi-calculus, the encoding can be used to push the logic for the typed fragment of the pi-calculus given by L, back to L itself, obtaining a Hoare logic for L.  Continued below.  
> **username_6**: This paradigm has now been used multiple times to obtain logics for programming languages that had been out of reach for other approaches to constructing program logics, including the first program logic for languages with call/cc [here](http://www.sussex.ac.uk/Users/mfb21/publications/fsen09/), the first logic for programming languages with ML-style extrudable local store [here](http://www.sussex.ac.uk/Users/mfb21/publications/fossacs07/index.html) and various distributed progamming languages (not yet published).  
> **username_2**: @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.  
> **username_6**: @Neel What is a good program logic is a highly interesting question that deserves more work, even if it's unlikely that a universally convincing solution can be found any time soon. However I don't think "simple programs should have simple proofs" is achievable, at least not for notions of simplicity that are somehow related to program/formula/proof length. The reason is that it's quite likely that many simple programs will have only long proofs. For example the specification (in a logic for total correctness) of Collatz's function C (with the parameter being free) {True} C {True}. (Ctd.)  
> **username_6**: The assertion {True} C {True} probably does not have a short proof (assuming the Collatz function always terminates) in any natural logic.   One option at this point would be to assume an oracle for Peano arithmetic, ZFC or whatever ambient formalisation of mathematics you are using, and look at the remaining proof length. This would 'measure' the contribution the rules and axioms for the programming language make to the complexity of proofs. If we take this point of view, our approach looks good: (Ctd.)  
> **username_6**: characteristic formulae can be inferred by induction on program structure, and if the program to be reasoned about has n constructors, the proof would have length n+1, with the +1 being the oracle invocation. However, this is misleading in that all we are doing in the first n steps is to translate the operational semantics of the program into (the relevant extension of) first-order logic. So we really only shift all the reasoning complexity to the oracle. characteristic formulae can be inferred by induction on program structure, and if the program to be reasoned about has n constructors, (ctd)  
> **username_6**: the proof would have length n+1, with the +1 being the oracle invocation. However, this is misleading in that all we are doing in the first n steps is to translate the operational semantics of the program into (the relevant extension of) first-order logic. So we really only shift all the reasoning complexity to the oracle. (Ctd.)  
> **username_6**: Regarding dropping magic wand from separation logic hardly affecting practical usability: I don't know much about separation logic, but could it not be an effect of selection bias: most algorithms verified in separation logic don't have much sharing going on, so you can happily make do with just separating conjunction?  
> **username_4**: @MartinBerger. I think what Neel is saying is that completeness theorems don't satisfy him.  If you can show him some good proofs of programs which are currently tricky to prove, then we could have a more productive discussion.  (Well, I am in the same boat!)  
> **username_6**: @UdayReddy. The predicate "currently tricky to prove" is vague. For any programming language, program and predicate that holds of that program, I can come up with a 'logic' where that predicate is trivial to prove. Conversely, for any logic with good universal properties, it's probably easy to come up with programs that are hard to prove, but that's got little to do with the programming language (e.g. diagonalising over the integers to find counterexamples to Fermat's last theorem).  

---

