On Two Views of Computation in Computer Science

> The hard fact is that, while you can reason about purely functional programs using little more than high-school algebra, reasoning about imperative programs requires bringing in the heavy apparatus of logic right from the start, because imperative programs denote predicate transformers.

1. It is immediately obvious that TLA+ is simpler than SML, yet as powerful as Coq; it is TLA+ that requires little more than high school math. You can reason with it about any kind of algorithm you like, using the same simple, familiar math (FOL, ZF plus three temporal operators, of which only one is really used for safety properties).

2. Imperative/functional is a language concept. In TLA+ there is no such thing as an imperative or a functional program. There is an algorithm that, say, computes a factorial in some sequence of steps. Is that sequence imperative or functional? Hard to say. TLA+ is pure, yet doesn't model an algorithm as a function.

3. Imperative programs do not denote predicate transformers. They denote whatever sound model you decide they do. The whole idea of "denotation" is a semantic one, i.e., tied to a specific language. E.g., in TLA+, all algorithms -- functional, imperative (although there's no difference), parallel, concurrent, quantum -- denote a set of behaviors, where each behavior is an infinite sequence of states.

Lamport's entire idea is that thinking of languages and semantics when reasoning about algorithms complicates things unnecessarily. Think of algorithms as abstract state machines, and reasoning becomes -- if not simple -- then as simple as possible (today, at least).

> Your use of induction on the program counter reveals that you're just using the program as a proxy for a class of computations.

That is what a program reasonably "denotes" (and what it, in fact, does in TLA+). But the proof works on the representation of the program, which is just a logical predicate.

> Um, no. Predicates don't express computation.

Um, yes, they do. In 1994 Leslie Lamport wrote a paper (2500 citations) that shows how they can, and that makes everything simpler. It is one of the best known and most widely used algorithm logics. It's nothing obscure.

> Would you have been able to produce your proof entirely by yourself?

Yes. First I thought of it, then I wrote it, then I added details until it checked. But let me tell you: if a proof assistant would ever make proofs easier than doing them in your head, then I'd be very happy. Usually they make things harder because they need lots of detail. Sometimes they're necessary if the proof is shallow but very big, and requires remembering lots of things. But, unfortunately, proof assistants don't help you uncover a proof. Model checkers can do that sometimes.

> What facilities for data abstraction does TLA+ have?

The full strengths of set theory (sets, functions), plus sugar for sequences and records.

> How do I hide the representational choices of a module I'm not currently concerned with?

TLA+ has a simple module system. Definitions can be local or public.

> First-order logic is not “high-school math”. You can't expect most high schoolers to know how to correctly manipulate logical quantifiers.

Depends on the country I guess. But OK, first year college.

> And axiomatic set theories (such as ZF), which are built on top of first-order logic, are definitely not “high-school math”.

None of that has any bearing on specifying algorithms, though.

> That's the thing: I want to reason in a time-independent manner as much as possible. Time-invariant reasoning is simpler and mathematically more beautiful than exploring state spaces alongside with your processes.

That's only because you're used to thinking in a way that is tied to languages. I have yet to encounter a powerful type system as mathematically elegant as TLA+.

> Then in TLA+ all algorithms are expressed as imperative programs.

No. They're expressed as nondeterministic abstract state machines, written as a first order logic predicate. Each step of the machine is arbitrarily complex. You can specify a program in TLA+ that in each step solves a difficult SAT problem, or even the halting problem.

Imperative is an attribute of a programming language with programming language semantics; TLA+ is ordinary math and doesn't have any of those attributes. It's like saying that calculus is imperative. However, it certainly isn't functional because it doesn't identify the concept of a function with the concept of a computation.

I guess you could specify a functional program as a machine that computes its result in a single state (although I wouldn't). You could then model, I don't know, LLVM machine code, and shoe that the machine code algorithm is a refinement of the functional program.

> By virtue of exploring large state spaces?

I don't understand the question. The reasoning -- as any other formal reasoning -- is done by manipulating logical formulas. The state space is a property of the model, not of the logic.

> Checked by whom?

TLAPS, the TLA+ proof system.

> Type inference reconstructs type derivations all of the time.

It's done reliably because the properties they represent are kept very computationally simple. In TLAPS uses SMT solvers to reduce the effort, and where a type would be inferred, so would a proposition. The problem is with more interesting propositions.

> every mathematical object (internal to your set theory of choice) is represented as a set (or urelement, but those are even weirder) somehow, even if the encoding is irrelevant for your purposes.

Yes, but it's completely opaque to a spec. There's no way of obtaining the representation of, say, a function. But let's not get into the debate of set theory pros and cons, because it really makes no difference.

> Hierarchical modules?

Yes.

> Parameterized module families?

I don't know what you mean, but you can instantiate the same module multiple times with different parameters.

> Multiple views of the same module, showing or hiding different aspects of it?

Not that I know of, but as modules are instantiated, you can instantiate them and import, and then export. I can't see this being too useful, though. TLA+ specs are usually small. A 3000 line spec (over multiple modules) is considered very big.

> You were the one who originally brought up ZF, describing it as “high-school math”, so I was just refuting that.

Those parts of ZF that are used in practice when writing a spec are high school -- sorrt, first-year college -- math. Come on. That people write PhDs on algorithms they implement in Python doesn't mean that Python isn't a high-school-appropriate language.

> If elegance is your only criterion, it's very hard to beat Martin-Löf type theory.

Actually, it's extremely easy, especially where algorithms are concerned. In TLA, deterministic, nondeterministic, parallel, concurrent, neural, quantum algorithms are all simple special cases, and even better: properties of algorithms and algorithms are the same object. Think of it as type theory with nothing but types, only using ordinary familiar math. That in any type theory a type is a different object from its inhabitants (even if types and programs can use the same terms), already makes it much more complicated than TLA+.

> Of course, usability matters too, and there MLTT fails miserably, at least for programming purposes. Higher-order dependent types don't come for free.

Right. Amazon, Intel, Oracle and Microsoft engineers use TLA+ all the time to specify and verify very large distributed systems.

> Prove them by hand. Good old-fashioned brain usage is never going away.

Sure. Except when you have a transactional distributed database algorithm to verify, that's kind of hard. But nobody has the time for deductive proof anyway. TLA+ comes with a model checker. You just press a button and if your assumptions are incorrect you get a counterexample.

> By the way, I'd like to see your full proof, for the exercise you posted a while back. (“Prove that there exists some i such that y[i] = 1 at the end of the whole computation.”) Is it as short and sweet as my proof?

Shorter and sweeter :)

Informally, it goes as follows.

This is our partial correctness property

    PartialCorrectness ≜ AllDone ⇒ ∃ p ∈ ProcSet : y[p] = 1

And this is the inductive invariant:

    Inv ≜ PartialCorrectness
            ∧ ∀ p ∈ ProcSet : pc[p] ≠ "Line1" ⇒ x[p] = 1

We need to show that Inv implies PartialCorrectness (trivial), that Inv holds in the initial state, and that if it holds in any state s, then it holds in any possible consecutive step s'. It's easy to see that it holds in the initial state. Now, let's assume it holds in s, and prove for s'. To make this transition, some process p either executes line 1 or executes line 2. If it executes 1, then PartialCorrectness doesn't change because no new process is done. The second conjunct holds because we've just left line 1 and x has been assigned (by the definition of line 1). If we are currently in line 2, the second conjunct of the invariant doesn't change. By the definition of this action, we'll be done. Here we have two cases, either we set y to 1, or we set y to zero. If we set y to 1, we're done and PartialCorrectness holds. If we set y to 0 then by the assumption of the invariant, the process we depend on must not be done, hence AllDone is false, and PartialCorrectness holds. QED.

Now, the machine-checked formal proof no longer looks so short and sweet because, well, it's completely formal and verified by a checker, so there's a lot of detail that's absent from an informal proof (I'd like to see you formally explain to a proof assistant: respecting the old interleaving, or even your inductive step). TLA+ proofs are written in Lamport's structured "modern" proof style: http://research.microsoft.com/en-us/um/people/lamport/pubs/p...

Also, note that I wanted to show this to someone else, and for pedagogical reasons I wrote the program in an imperative language called PlusCal that is then compiled to TLA+. In TLA+, the "program" is the formulas Init and Next. They are combined to form the temporal formula Spec. A non-modal subformula means that the condition holds in the first state of the behavior. A square operator ("always") means that the subformula holds in all suffixes of the behavior (and a diamond means that it eventually holds). The square brackets with the "vars" subscript has to do with stuttering, which is important for composition and refinement, but I won't explain it here.

Here is the spec with the formal proof: https://www.dropbox.com/s/7i239785jngat2b/Foo.pdf?dl=0

Ah, but that's not my question! My question is whether the specifications we are interested in implementing in practice are hard in theory.

That's a good question and I don't think anyone has a definitive to that. I certainly don't. I think we should do empirical research and try to find out. What would be your guess and why?

I do have a some ideas, though. First, I think that the effort required for end-to-end proofs -- even for heavily simplified, relatively small programs -- does indicate that the problems are inherently hard because I don't think we're lacking some secret proof technique that would all of a sudden make things significantly easier. The difference between cases that are extremely hard (Goldbach's conjecture) and real world code doesn't seem big. Second, I think that empirical research might uncover something that can have a bigger impact. End-to-end proof is not a very important practical problem, because very few software projects ever need it or anything close to it. Improving correctness or reducing development costs (two sides of the same coin) for non high-assurance programs is much more important, and where the theory leaves much more wiggle room (because once you step away from actual watertight proof, basically anything is possible). I believe that empirical research can uncover certain common program patterns and bugs that can be analyzed/prevented, and that those may give a significant boost. But without empirical research, we won't even know which patterns/bugs to tackle.

I think that emphasis on deductive proofs is misplaced (in light of theory and practice) as it's hard to fine-tune[1], and indeed, the software verification community has been moving further and further away from that direction for a long while; since the seventies, I believe. It's the PL community that's decided this is interesting to them. Software verification is interested in many other approaches, like static analysis (that can verify some properties -- hopefully important -- some of the time), probabilistic methods, combination of formal methods and testing (like so called "concolic" testing) etc..

------

[1]: I'm referring to actual proofs with dependent types. Simpler type systems can be invaluable, if researchers only tried to figure out which properties are actually important. For example, Rust's borrow checker is extremely interesting, and tackles a class of bugs that's known to be both very harmful and easy to prevent mechanically. We should be looking for more of those. An example of what not to do if you want real-world impact, is the peculiar focus on effect systems. Other than shared state (which is a whole other matter), how did some PL researchers get it into their minds that effects are an important problem to tackle?