On Two Views of Computation in Computer Science

Yep, that's the state of the art. It means that more human work has to be done on making it easier to write programs that work.

> The same function may be computed by different procedures with different complexity.

The whole idea of computational complexity theory, the time- and space-hierarchy theorems, that are generalizations of the halting theorems and are probably the most important theorems in computer science, is that every function has an inherent complexity, that is independent of the algorithm that implements it. The time or space complexity of an algorithm may be greater than or equal to the complexity of the function. You may want to read my blog post about computational complexity in the context of software correctness: http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...

> Not all types denote sets

In this case, what matters is what set they specify (not necessarily denote) and what proof.

> This is the price of capturing the meaning of computation. Of course it doesn't come for free. But, in general, the earlier you do it, the less work it requires. In the limit, if you do it really late (e.g., test suites), it requires an infinite amount of work (searching infinite input spaces).

First, the computational complexity of verifying a program is the same no matter when it's done. Read my other blog post. Second, I'm talking theoretical computer science here. Obviously there are all sorts of interesting trade offs in real world programming. Finally, the whole point of this article is that language models do this extra computational work and solve a different problem, while the people discussing them often don't notice or point this out.

> TLA+ is groundbreaking, if it satisfies your description.

Thing is, TLA+ does what specification languages are supposed to do. It is just an exceptionally small and elegant specification language. It may feel like groundbreaking to people who have never used specification languages. Haskell is not a specification language. It's a programming language, therefore it is much more complicated -- like all programming languages -- and much weaker -- like all programming languages. There are programming languages that seek to do what both specification languages and programming languages do. Examples include SPARK, Coq, Agda. Of them, the only successfully used language is SPARK, but it is limited as a programming language. Coq and Agda have never been used for large programs, so nobody knows if they work at all. Early results (like CompCert) are not promising. TLA+ is used on very large projects every day at Amazon, Oracle and Microsoft. No academics are involved. Same goes for other specification languages like Z.

Because for years the PL community has been trying -- without success -- to combine a specification and a programming language into one, someone who's familiar with programming languages may view specification languages as groundbreaking, but they've been doing their job for decades. They just don't try to do what the PL community is trying which is to also serve as programming languages. Once you give that up, the things you want and that are so hard to get become much easier.

Here's how things become easier:

1. There's a result (mentioned in my Curry On talk/post) that simply put states that correctness doesn't compose. In intuitive terms, if your program consists of 10,000 functions, each 3 lines long, composed in various ways, you can't prove global properties by doing simple proofs that are as easy as you'd expect for 3-line functions, and have the global result pop out. The idea of the proof is very simple: in computations, complexity builds up very fast. A TM with 6 control states can have 10^35,000 states or so, and states in sub components simply cannot be hidden. The way to tackle that is not to try to prove the global properties directly from the local properties, but to describe the entire program in various abstraction levels and then prove that each lower level refines the higher one. This is very hard to do in programming languages at scale. In a specification language, you have better control over level of abstractions and what details you want to leave out.

2. There's nothing external; I.e. there's no IO. An example of something that's very important to prove is, e.g., if you read a certain record from the DB many times, its "last_updated" field gorws monotonically. I don't know how you can try to do it in a programming language. In a specification language, you specify the entire system -- the DB, the network, the OS, the users -- and you do it in the abstraction level that precisely suits your needs. There is no information overload and no missing information. You write your assumptions, and hope to get verification for your claims.

3. There's no need for efficiency. You can freely use simple mathematical definitions whose "automatic" implementation is extremely inefficient, because the code never gets executed.

So, specification languages work, and have worked for a long time. What doesn't work is a specification language that's also a programming language. That would be truly groundbreaking, but I don't think anyone is even remotely close, or is even looking in the right direction.

> I suppose I could go Googling for info on how TLA+ is composable but if you know the answer yourself why not explain it or point me to a specific article which explains it?

See chapter 10 of this freely downloadable book http://research.microsoft.com/en-us/um/people/lamport/tla/bo...

The problem here may still be that you're thinking of composability in terms of functional languages instead of composability of abstract programs. The book does not translate the terms you're familiar with to TLA+ terms because it doesn't assume any existing predilections. For example, you're used to thinking of the "map" function as a higher-order algorithm. That doesn't mean that's what it is; that's just how it's described in Haskell. Another way of looking at it is that map is nondeterministic. The book won't tell you that what you know as parameterization is just another form of many of nondeterminism (concurrency, IO are other forms). If you have nondeterminism as a built-in construct, there's no need to work hard on higher-order things; they're just special cases. But, again, the book starts "from scratch" and doesn't assume that you're used to thinking in Haskell. So there's no lack of material; there just isn't a dictionary for people who are already used to thinking about things in some specific way. I hope to write such a dictionary one day.

> Absolutely, and thus types and specification via TLA+ are not in opposition. In fact they can work in harmony.

Sure, it's just that TLA+ can open your mind to the idea that you may not need types for things you think you do -- even in a programming language. It can also show you how you can do mutation and still remain pure without using monads or any higher-order function composition. This idea is used in synchronous programming languages, too, so this is something that definitely applies to programming languages.

> Indeed, even the fundamental TLA+ notion of "priming" variables seems that it would immediately be an impediment to composability.

Why? It's a perfectly pure operator and it distributes. Op(x, y)' = Op(x', y'), assuming Op doesn't have any other variables in it, i.e., it's a "level 0" operator.

> Correctness does compose in my experience as a mathematician

I can show you a trivial example of why that's not true: the gravity equation. Everything composes, yet two instances are already chaotic. You can't extrapolate almost anything you know about the gravity equation to predict the bodies' positions over two instances. For discrete processes, such chaotic behavior is small potatoes. We don't even use the word "chaotic" because we're way beyond that. The problem is this: if everything is simple, you can compose correctness. But when everything is simple, composition isn't really required. This is what I'd like to call the "FP extrapolation problem". FP works beautifully for simple examples, i.e., where new approaches don't really matter. People then extrapolate from toy examples and assume it can scale (in spite of the theory that says otherwise), yet no one has yet shown that it does in practice. By that I don't mean that you can't write large programs in FP. Of course you can. But the advantages that are very clear in the simple cases (where they don't matter), start dissipating and you just don't see a drastic effect at scale (maybe the effect is even negative; nobody knows).

> Please explain your terminology.

Sorry, I meant a TM that terminates eventually. I think that's either the current record or the lower bound. Don't remember.

> I find this a very puzzling statement. States in subcomponents can be easily hidden in every common-or-garden programming language.

They're hidden from the programmer's view, not from their effect on correctness. That is precisely the result that says that verification isn't fixed-parameter tractable. Namely, if the cost of verification is O(|S|) when S is your number of states, you can't say, well, each of my components has n states and I verified them individually, and now I want to compose k components, and so the cost of verification would be O(small function of k). It will be O(n^k) or something like that.

> Sure, but as we've observed, it doesn't actually tell you anything about the final implementation you come to write.

Right, but nothing else can, either, unless you do end-to-end verification, which is far beyond what 99.9% of projects can afford to do (or need to). Here is where you rely on software engineering practices, tests and whatever tools you have for local properties that help prevent easy bugs (like types and static analysis). There is nothing that can help you prove interesting logical properties at this level, at anything close to an acceptable cost.

> What does it mean to you?

Oh, the same. It just doesn't look the same way in TLA+, where you compose things as A ∧ B rather than A(B) (they don't mean the same thing).

> What exactly does that mean?

Alright, let me try: suppose you have a higher-order function, say `filter`, that takes a function of type `a -> bool` (where a is a type parameter), and filters a list. Now suppose you want to prove that, say, the length of the resulting list is no bigger than the input list. In a functional language you say, I have a function parameter `p` that could be anything of the appropriate type `a -> bool`. In TLA+ you don't need this because you can say that p is not a parameter of a certain type, but a concrete, specific program that nondeterministically returns either TRUE or FALSE. You prove your theorem for that specific p, but it really covers the same as all predicates p of that type.

The cool thing, then, is this: you can ask, what is the relationship between that nondeterministic program p, and a deterministic program p1, that, say, returns true iff its argument is an even number? Well, it's a refinement relation (any behavior of p1 is a behavior of p, but not vice-versa), and in TLA+ this is expressed simply as p1 => p, where => isn't some special notation but the same-old familiar implication operator from propositional calculus, because in TLA+, a program is a binary boolean predicate that evaluates to TRUE iff there's a next-state relation between its two input states, the unprimed and primed.

The key to that is understanding the model (in the logical sense) of a TLA formula (i.e. a program). The model is a set of all possible behaviors, where a behavior is a sequence of states (similar, but not exactly a trace in the process-calculi sense). So a program is a set of behaviors. A program property (i.e., the program never sends the character "x" over the network), or a "type", is the set of programs that satisfy it (I mean by the simple isomorphism between predicates and sets). Here is the crucial bit: as the TLA logic only allows to specify properties that must be true for all behaviors or none (hence the problem with probabilistic algorithms), there is no need to keep the behavior sets for each program in the "set of programs" separated, and instead of a set of programs -- i.e. a set of sets of behaviors -- a program property can simply be a set of behaviors. But a set of behaviors is a program! Therefore a program property, or a "type", in TLA is the same thing as a program. Program properties and actual algorithm specifications become a hierarchy of nondeterministic programs that refine or abstract one another. So the program that does parallel merge-sort is a refinement of a program that does some sort of merge sort, and that, in turn is a refinement of a program that "sorts somehow". And all those relationships are simple propositional calculus connectives, and you can reason about what kind of low-level steps a low-level specification does for each abstract step in a higher level specification.