(0) Computational complexity. Neither the lambda calculus nor Turing machines were invented to answer questions of computational complexity.
(1) Functions at types other than `nat -> nat`. Curiously enough, programming in the real world is seldom about evaluating functions of type `nat -> nat`.
Since computers regularly implement exactly such a mapping, it doesn't sound like a problem.
>Curiously enough, programming in the real world is seldom about evaluating functions of type `nat -> nat`.
How is it not about that? Everything you do is converted down to CPU ops that just implement (something expressible as) functions on natural numbers (technically, fixed-with binary numbers). The whole job of programming can be described as "converting a problem to a format suitable for a fast `nat->nat`-implementing machine"; it's just that several of the layers of the conversion are hidden from you.
That's the thing. In some languages, this mapping doesn't always exist.
> AIUI, the CTT is equivalent to saying that anything that can be computed at all (regardless of type signature) can be done via the `nat -> nat` functions representable on some TM.
The Church-Turing thesis says absolutely nothing about abstraction barriers your language might enforce, e.g., what you get if your language has parametric polymorphism (and no means to circumvent it, e.g., reflection).
These abstraction barriers might seem just like limitations that buy you nothing, but that's not the case. For example, if your language has abstract types (not the same thing as abstract classes), then you can be sure that any internal invariant violations can be traced to the module where the abstract type is defined. Have fun getting a static guarantee of this kind in C or Java.
> How is it not about that? Everything you do is converted down to CPU ops that just implement (something expressible as) functions on natural numbers (technically, fixed-with binary numbers).
Compilation translates programs in a source language into semantically equivalent programs in the target language. Compilation doesn't guarantee that every target language program is expressible in the source language - in fact, this is often not the case.
The mapping exists, just not necessarily within the language; the CTT is orthogonal to practical difficulties of massaging the data into a usable input format. (e.g. how to convert a binary tree in to the TM's format and vice versa)
>The Church-Turing thesis says absolutely nothing about abstraction barriers your language might enforce, e.g., what you get if your language has parametric polymorphism ...
Those all speak to the issue of how difficult it is (for e.g. a human) to implement the function, not whether language/computation model can compute it at all.
>Compilation translates programs in a source language into semantically equivalent programs in the target language. Compilation doesn't guarantee that every target language program is expressible in the source language - in fact, this is often not the case.
If you have a computation for which no TM (or asm, C, etc program) exists that computes it, let us know! That would be real progress on the CTT towards a negative answer and a Fields Medal for whoever found it!
In practice, people write their programs in a programming language. Some languages (e.g., C, Java, Lisp) only provide leaky abstractions, so programmers always have access to the internal representation of everything, to the detriment of modularity. But there are languages (e.g., Standard ML) that aren't hobbled in this way.
> Those all speak to the issue of how difficult it is (for e.g. a human) to implement the function, not whether language/computation model can compute it at all.
No. In Standard ML, writing a function that inspects the representation of an abstract type isn't “difficult” - it's literally impossible. If you want to do it, you have to use a different language. The type system enforces the separation of concerns, so that you don't have to rely on your discipline alone.
> If you have a computation for which no TM (or asm, C, etc program) exists that computes it, let us know!
Re-read my sentence. I was talking about the converse: There exist programming languages that don't allow you to do everything the target machine can do.
For an analogy, you can map all the natural numbers to real numbers. This proves just about nothing. That you cannot map all the reals to the naturals proves something very important.
It would be truly bizarre if a useful programming language could express something that computation on bits could not.
If you can't map higher-order constructs to Gödel codes (effectively, numerical representations of syntax), you can't always map them to `nat -> nat`. That's precisely my point.
And, if you could map higher-order constructs to Gödel codes, the higher-order abstractions would be lost - all you need to do to break the abstraction is inspect the syntax. Just like, if you have reflection, type abstraction is lost - all you need to do to break the abstraction is use typecase.
As long as f(n) outputs a unique m, you can number f, n, and m. And as long as a programming language is Turing complete, you can do that. Interpreting any sort of abstraction is beside the point (even the "Gödel sentence" that you could ultimately find needn't be interpreted... which I suppose in this case would be a "Gödel operation").
Insofar as a program can be compiled and implemented in machine code, all the functions of that program's programming language can be mapped 1 to 1 to nat -> nat operations. This is just what's at issue here.
To cut through it a bit, you write
> The Church-Turing thesis says absolutely nothing about abstraction barriers your language might enforce, e.g., what you get if your language has parametric polymorphism
If a language has parametric polymorphism, is it therefore not Turing complete? Because if the language with parametric polymorphism is Turing complete, then the Church-Turing thesis absolutely has something to say about that language.
That mapping is a property of the implementation, not of the language. A user of the source language can't rely on the existence of this mapping - it would be literally impossible to run programs, say, using paper and pencil.
> If a language has parametric polymorphism, is it therefore not Turing complete?
Whut?
> Because if the language with parametric polymorphism is Turing complete, then the Church-Turing thesis absolutely has something to say about that language.
It says something about the functions of type `nat -> nat` that I can compute in the language. But a language with parametric polymorphism has lots of other types besides `nat -> nat`.
Alright, at that point it becomes an issue of "what kinds of things count as computations" for the purposes of the CTT. You're right that some languages simply lack certain capabilities, but that's an issue of access, not computation per se. You can get the same result in pure math:
"C is incapable of computing the zlobnorg of a matrix."
'Ridiculous! I'm sure I can write a program that does it! So, what exactly is a zlobnorg?'
"Sorry, only the matrix itself can answer that."
If you're going to go that route, then yeah the CTT is false -- likewise, TMs can't see inside black holes, so they can't "compute" that either.
But the "computations" referred to in the CTT are assumed to meet certain criteria, e.g. that there's some API exposed for accessing the relevant information, and the output is a "pure function" of that input (or at least makes any external state changes accessible, etc). But then once you've done so, all the Turing-complete languages can access said information information and compute the correct result.
Now, if your point is that the day-to-day work of a programmer is a lot more than writing pure functions: I whole-heartedly agree and have said the same thing myself. I cringe at the whole "Maxwell's equations of programming". Of course you have to care about external state and access privileges and race conditions and whether the API is usable, etc -- things that the CT notion of "computation" doesn't deal with. But, for the same reason, that's also orthogonal to the CTT.
Types determine what computations make sense.
> If you're going to go that route, then yeah the CTT is false -- likewise, TMs can't see inside black holes, so they can't "compute" that either.
Careful! I never said the CTT is false. I only said it guarantees nothing about functions whose type is anything other than `nat -> nat` (up to isomorphism).
> But the "computations" referred to in the CTT are assumed to meet certain criteria, e.g. that there's some API exposed for accessing the relevant information (...) Of course you have to care about external state and access privileges and race conditions and whether the API is usable, etc
These are properties of programs, not functions. Two syntactically different programs may compute the same function, so you can't conflate programs with functions (and hope to make sense).
Types determine what the developer has certified as making sense. There can (and as far as we know, always does) exist an isomorphism between the higher-typed function that the developer has implemented and the TM-computable nat->nat.
So, a TM can "make sense" of the higher-order function, even when it only has the nat->nat type.
>Careful! I never said the CTT is false. I only said it guarantees nothing about functions whose type is anything other than `nat -> nat` (up to isomorphism).
And and I was saying that the CTT is equivalent to saying that there is an isomorphism between a TM-computable nat->nat and any function that can be computed at all.
>These are properties of programs, not functions. Two syntactically different programs may compute the same function, so you can't conflate programs with functions (and hope to make sense).
Fair enough -- I should have said "function" there but the point stands: you can't refute by CTT by defining Turing-complete language that lacks some critical access and say, "well, that's a function I guess it can't compute!"
Types determine what computations make sense, even before any program is written at all.
> There can (and as far as we know, always does) exist an isomorphism between the higher-typed function that the developer has implemented and the TM-computable nat->nat.
Are you sure you're talking about isomorphisms in the mathematical sense? https://ncatlab.org/nlab/show/isomorphism I'm talking about a pair of morphisms:
forward :: Foo -> Bar
backward :: Bar -> Foo
backward . forward = id :: Foo -> Foo
forward . backward = id :: Bar -> Bar
> And and I was saying that the CTT is equivalent to saying that there is an isomorphism between a TM-computable nat->nat and any function that can be computed at all.
What category are you working on?
> you can't refute by CTT by defining Turing-complete language that lacks some critical access and say, "well, that's a function I guess it can't compute!"
I'm not refuting the Church-Turing thesis! Why would I want to? I even believe it's true... in some models. (Yes, truth is relative to models of a theory. Unlike provability.) I'm only saying that the CTT only claims what it claims. You're making extra conclusions that don't follow from the CTT's statement.
>Types determine what computations make sense, even before any program is written at all.
>What category are you working on?
I have no idea what point you're trying to make with either of these comments.
>I'm not refuting the Church-Turing thesis! Why would I want to? I even believe it's true... in some models. ...
Regardless, my point is that the limitations you're bringing up seem to be very trivial and understate the extent to which it does apply. You're still wrong if you think the CTT is "true, but false if applied to matrix functions. No way could a computer handle that. They only know binaries numbers, not the matrix type. I mean, come on, I gave them a different name and everything!"
The inhabitants of the type `forall a. a -> a` (which, by the way, in an effectful, Turing-complete language, has more inhabitants than just the identity function) aren't in one-to-one correspondence with the inhabitants of the type `nat -> nat`. I asked for an isomorphism of types, you have to give me an isomorphism of types. Or maybe you don't know what “isomorphism” means in mathematics?
>> What category are you working on?
> I have no idea what point you're trying to make
Okay, you don't know what “isomorphism” means in mathematics.
> You're still wrong if you think the CTT is "true, but false if applied to matrix functions.
The CTT isn't “false if applied to matrix functions”. The CTT says nothing about functions at a type not isomorphic to `nat -> nat`. It would be like saying “SilasX is all wrong about frogs!”, when you never said anything about frogs (at least, in this discussion).
> No way could a computer handle that. They only know binaries numbers, not the matrix type. I mean, come on, I gave them a different name and everything!"
I write my programs in high-level programming languages, not machine language, though. The whole point to high-level programming languages is to reason in terms of their abstractions, not their possible implementations.
No argument about it. But notice that this applies to programmers, not computers.
The article is about two groups talking past each other because of different terminology. When you say that "programming in the real world is seldom about functions of nat -> nat" you are doing the same, due to badly defined meanings of "programming" and "functions".
It applies to computers, because it's the computer itself that's preventing you from giving it certain classes of wrong instructions. I'm talking about enforcing things mechanically (type checking), not socially (design patterns, best practices, etc.).
If you consider that data to be a program, and the resulting messages to be errors, that is completely up to you.
As far as a typed high-level programming language is concerned, a syntax tree that doesn't type check isn't a program, so the question of what it does at runtime is simply ill-posed.
This is how Krishnaswami frames things. From the TOC perspective, there is no such thing as functions at all. Computations consume and produce strings. Both Church and Turing explain how those strings can encode the natural numbers (there was no talk of types by either). Interpreting a computation as one computing functions on the natural numbers or any other set is an entirely interpretive activity that is external to the computation itself.
Note: Next step down are analog components that are basically specific functions on real numbers. That's what I got from studying analog computers anyway.
It also seems kind of ironic to have the functional programming people in the camp that says that there's no such things as functions...
https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis#S...
I could choose a function between any two countable sets, e.g. (Nat -> Nat) -> (Nat -> Nat): pick a representation for the input and output and all models can compute the same functions, and those are the functions that machines can compute. They differ in abilities regarding representation within the model, but as the language models' representation require very significant computational work, I'd expect their representation to do more: they're paying for it.
A C compiler works hard, so you'd expect it to provide you with a representation more suitable to your wishes than machine code. It's just that as a compiler like C translates a "meaningful" language to a machine encoding, everybody notices the work. The language "computation" models work in a vacuum, so I just pointed out that even though they don't translate anything from one representation to another, they still have to pay for their natural representation.
There isn't a TM-suitable representation for things of type (Nat -> Nat). No matter how you try to encode a Nat->Nat as a Nat (or a bitstring, if you prefer), you're going to screw up equality (which means you're actually encoding some other type). You'll map two unequal functions to the same Nat, or (more likely) map one function to multiple unequal Nats. This is the difference between how lambda calculi and Turing machines handle higher-order things: A Turing machine can always inspect the "internals," so you need an actual bijection from functions to strings, whereas lambda calculus hides the internals, so it's safe to map one function to multiple syntactic representations.
If the benefits of multiple representations of the same value aren't clear from this example, consider a more mundane one: red-black trees as representations of ordered sets. For obvious efficiency reasons, it's not desirable to assign to each ordered set a canonical red-black tree representation.
This shows that the concept of a type requires actual computational work rather than just a matter of “free” perspective. Your mere presentation of a function as an inhabitant of a type creates a computationally harder problem than presenting a function as a mapping between sets. Put differently, when a typed language model computes a function (Nat -> Nat) -> Nat, it does more work, and solves a harder problem than necessary to compute that function in the normal set-theory sense. You can choose to solve that problem on a TM by simulating type checking if you like, but you can’t compare “compute a function in the set-theory sense” and “compute a function in the type theory sense”, because those are two different problems with two radically different computational complexity costs. You can decide to do that extra work or not (you may want to because you gain benefit from it), but you can’t compare a model that always does — and pays handsomely for it — with one that doesn’t.
Otherwise, I could create a language model that solves all NP problems in polynomial time by defining my language as requiring a proof certificate with every input problem, which my model would then check in polynomial time. No one would believe my language actually really solves a computational problem: it simply pushes the difficulty to the collaborator.
Equality is also an internal question. Define any relation between two sets (your definition of equality), and all models would be equally able (or unable) to decide it.
People who use set theory as their foundations impose on themselves the even harder task of making sure their mappings are coherent w.r.t. whatever notion of structure they want to work with, i.e., homomorphisms in a category of interest.
> Otherwise, I could create a language model that solves all NP problems in polynomial time by defining my language as requiring a proof certificate with every input problem
No, this is wrong. Changing the input type means that you are not, in fact, solving the original problem.
Let's not get into this old debate because we'll never get out of it. Suffice it to say that it that there is no doubt that Turing and Church (and Gödel and von Neumann) used set theory as their foundation, and when they said "function" they meant a set-theoretic function, namely a mapping from a domain (set) to a range/co-domain (set). If by "function" you mean a type-theoretic function then you're talking about a computationally harder problem, as you need to compute the underlying set-theoretic function and check a proof. You can certainly ask a TM to simulate a type checker and compute a type-theoretic function. There's actual work involved, and someone must do it. You cannot say that your formalism gives it to you for free, or you'll have a formalism that proves things for free, which is impossible.
> Changing the input type means that you are not, in fact, solving the original problem.
Exactly! But that is precisely what you do when you interpret "function" to mean a "type-theoretic function", and solve a different problem. Any work that needs to be done under the normal meaning of "function" also needs to be done in the typed formalism. If you need to ensure/prove something, there is work and computational complexity involved. Pushing it to a collaborator doesn't make it disappear (let's call this the law of preservation of computational complexity). Someone has to do it, and in no model does it suddenly become free. It's perfectly OK to say that you start counting after much of the hard work is done, but in that case you need to say that your model requires upfront work, and therefore cannot be compared to models that don't. That's my whole point.
BTW, any logical formalism forces you to pay attention to meaning; choosing to encode the logic in types has advantages and disadvantages, but it is not at all the only way to logically describe a program.
Pray tell, what's the use of a computation without paying attention to its meaning? My use case is simply “knowing the meaning as early as possible”, and there ought to be no discussion that this should be everyone else's use case as well. Nobody performs a computation without some sort of expectation about the relation between the inputs and the outputs.
> BTW, any logical formalism forces you to pay attention to meaning
I never said types are the only way. For instance, you could use Hoare logic, but it's notoriously more difficult to use, precisely because it gives programs no a priori meaning.
First, I don't think that the only way to assign meaning to computation is by formally assigning meaning to the syntactic components that comprise its program, as written in some human-readable language. Most of the relevant meaning is in human interpretation of the input and output or the sensors and actuators. Components' meaning may be stated informally. I am not aware that formal meaning is the only valid meaning. People wrote the software that landed men on the moon in assembly; that was pretty meaningful. I believe this is still the prevailing view in computer science.
Second, you keep identifying the notion of computation with the notion of a program written by a person. The theory of computation, from its earliest days -- by Turing himself -- has studied computational phenomena in neural networks, genetics (Turing was a pioneer of both NNs and genetic algorithms) and quantum phenomena. Some of the greatest achievements in CS are not specifically related to software (I count at least 20% of all Turing awards).
> For instance, you could use Hoare logic, but it's notoriously more difficult to use, precisely because it gives programs no a priori meaning.
Or TLA+, which makes types notoriously more difficult to use by comparison.
Please suggest alternatives - that actually work.
> Most of the relevant meaning is in human interpretation of the input and output or the sensors and actuators.
The relation between the input and the output. This can only be stated formally.
> Components' meaning may be stated informally.
That leads to disaster very quickly.
> I am not aware that formal meaning is the only valid meaning.
Well, I am. Too much nonsense has been said as a result of not formalizing things.
> Second, you keep identifying the notion of computation with the notion of a program written by a person.
No. Even if a computation “arises in nature” (which is just your way of looking at things, actual physical phenomena is what you can measure, plain and simple), the only way to make sense of it is to write a program that reproduces the computation. This is how scientific theories work.
> Or TLA+, which makes types notoriously more difficult to use by comparison.
Some type systems are more difficult to use than others, and the type theory community is definitely guilty of not paying enough attention to usability, but I don't see how model checking has a higher power/cost ratio than sensibly designed type systems. Which tool satisfies the following criteria?
(0) Compositionality: you can understand a large system by studying its parts in isolation.
(1) Handles higher-order constructs (first-class functions, objects) gracefully.
(2) Stops you from saying nonsense as early as possible.
I rest my case.
AFAIK, the only languages that fully express the computational meaning formally with types are the dependently typed ones. AFAIK, there has been exactly one non-trivial real-world program written in such a language, and its author wasn't too pleased with the process (I'm referring to CompCert and Xavier Leroy). Every other program in every other languages has most of its meaning expressed informally, in the mind of the programmer. Unless you believe that no programs work, then nearly all programs that do express most of their meaning informally.
> Too much nonsense has been said as a result of not formalizing things.
Formalizing things doesn't imbue them with good sense. You can state plenty of nonsense formally. The only thing you're guaranteed is that it's consistent nonsense, and, as someone said on one of my favorite TV shows, "The sole virtue of the ineffectual is consistency".
> Which tool satisfies the following criteria? ...
TLA+, and far more elegantly and simply than any typed language you've seen.
> TLA+, and far more elegantly and simply than any typed language you've seen.
Still eagerly awaiting your elegant and simple explanation of this! It sounds groundbreaking (genuinely).
https://www.microsoft.com/en-us/research/wp-content/uploads/...
and an older paper covering an interesting theoretical property has over 1000. Also, the author did get a Turing award -- not primarily for this, but it got a mention. So yeah, we're talking about a very well-known formalism in software verification, and people were impressed. I don't know about groundbreaking because the community is different. In software verification you get points for new proof methods and such; not necessarily for creating an elegant language. TLA+ is about finding the ideas that have been shown to work at scale, and creating a very elegant, minimalist language to express them, based on simple ordinary math as much as possible.
There is no shortage of good tutorials (especially considering how simple TLA+ so there's no need for 500 tutorials on monads), and the language was designed for and is used by engineers in industry working on large, complex systems. Companies that have started to use TLA+ (or use it extensively) on large systems -- Amazon, Oracle and Microsoft -- report that their engineers pick it up on their own from available materials in two weeks (that was my experience, too; it's easier than most programming languages). But those are tutorials and don't focus on the theory. Amazon published two excellent technical reports, one in CACM, about their experience, with pretty good data (that's what convinced me; I'm impressed with what's been shown to work in the field).
There is also no lack in more academic, theoretical material, but, as usual, that is mostly concerned technical details.
What's missing is a brief overview of the theory. I'd read at least the introduction to the original paper above, this 4-page historical note[1], and this[2].
[1]: http://research.microsoft.com/en-us/um/people/lamport/pubs/c...
[2]: http://research.microsoft.com/en-us/um/people/lamport/pubs/s...
Your point would be so much more effective if you could bring yourself to avoid having a dig at other technologies.
> I don't know about groundbreaking ... TLA+ is about finding the ideas that have been shown to work at scale, and creating a very elegant, minimalist language to express them
TLA+ is groundbreaking, if it satisfies your description. I have never found anything that hits the sweetspot of elegancy and simiplicity along with robustness and composability as well as Haskell does. I'm not ideological about this. That is simply my practical observation borne out of a couple of decades of experience writing software. If TLA+ is genuinely better than Haskell on those axes then I'll be delighted to switch without a second thought. I am hoping to be convinced!
> I'd read at least the introduction to the original paper above, this 4-page historical note[1], and this[2].
I read them ages ago when you first suggested them to me. The impression of TLA+ I got was far from compelling in the composability stakes. 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?
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.
> someone who's familiar with programming languages may view specification languages as groundbreaking
That's not what I find groundbreaking. What I find groundbreaking is that TLA+ is (supposedly) so composable despite being so simple. I remain skeptical. Indeed, even the fundamental TLA+ notion of "priming" variables seems that it would immediately be an impediment to composability.
> There's a result (mentioned in my Curry On talk/post) that simply put states that correctness doesn't compose.
Yes, I recall that. I believe the theoretical result, of course, but I am yet to be convinced of its practical relevence. Correctness does compose in my experience as a mathematician and as a software developer. In fact, I can't see any way that correctness can be achieved except through compositionality.
> A TM with 6 control states can have 10^35,000 states or so
Please explain your terminology. Surely it can have infinitely many states? Indeed a Turing machine with 1 control state can have infinitely many states.
> states in sub components simply cannot be hidden
I find this a very puzzling statement. States in subcomponents can be easily hidden in every common-or-garden programming language.
> You write your assumptions, and hope to get verification for your claims.
Sure, but as we've observed, it doesn't actually tell you anything about the final implementation you come to write.
> The problem here may still be that you're thinking of composability in terms of functional languages instead of composability of abstract programs.
I'm thinking of composability in terms of building things out of smaller things and being able to deduce properties of the things based on the properties of the smaller things. That notion precisely captures "composability" (even "compositionality", if we want to get formal) as far as I am concerned. What does it mean to you?
> The book won't tell you that what you know as parameterization is just another form of many of nondeterminism
OK, but you could. What exactly does that mean?
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.
I'm very much hoping this will be the case!
> > 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')
Why? Because:
> assuming Op doesn't have any other variables in it, i.e., it's a "level 0" operator.
That's not an assumption I want to have to make! Since I don't understand this specific example perhaps my challenge here is unwarranted, but in general if I have to "assume" anything then that's an impediment to composability.
> 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
OK, I think I see. You prove something using the specific, concrete p which has fewer properties than any other p, so therefore anything that holds for it must hold for the other p too. I don't quite see how this is different from proving it for "arbitrary p" but perhaps it will be come clear as I learn more.
> I mean by the simple isomorphism between predicates and sets
And this is why I get worried about TLA+ using "simple mathematics". This "simple isomorphism" simply doesn't exist, as I'm sure you know. You have to restrict yourself to saying "simple isomorphism between predicates on a set and subsets of that set", at which point I start to worry that any higher-order possibilities go out of the window.
> But a set of behaviors is a program! Therefore a program property, or a "type", in TLA is the same thing as a program.
Sure, but a possibly nondeterministic one that you can't actually implement (at least not directly).
Anyway, thanks for the introduction. When I get some time I will look into it further.
You don't need to make that assumption, though. TLA+ checks it for you. My point is that everything is pure and well-behaved. The very same issues of modality happens when you use monads. Only in TLA+ it's very simple to see when an operator is a constant (called level 0), a state function/predicate, i.e., a function of the current state (level 1), an action/step (level 2), or a full temporal formula (level 4). In a temporal formula, you can say something like, whenever my program sees an event x, it would eventually output a response y. In a way, TLA+ has 4 syntactic types, and the relationship between them is checked instantly at parsing. E.g. you can't take an action or a temporal formula and prime it (TLA+ checks "inside" your formula and knows what level it is). Priming a constant keeps it a constant; priming a state function turns it into an action (a relationship between two states).
> This "simple isomorphism" simply doesn't exist
No, I meant something very simple. Any boolean predicate, e.g. "this number is even", is the same as the set of all even numbers. It's a characteristic function. It always exists.
> Sure, but a possibly nondeterministic one that you can't actually implement (at least not directly).
Right, but nat -> bool, is the same as saying "all programs that take a natural and return a boolean", which is the same as the ND program that for any natural nondeterministically returns true or false. It's describing the same set or type, but in a different way, which makes simple logical implication the same as subtyping or type inhabitance. B is a subtype of A, is, in TLA+, B => A. a is an instance of A, is in TLA, a => A.
BTW, it's not true that TLA+ can't tell you that your implementation is correct. It can, it's just hard (but probably no harder than in Coq). What you do is, you write a high-level model and prove it. Then you implement it in a programming language, and you write a compiler from that language to TLA+. Then you check that the TLA+ version of your implementation is a refinement of your high-level model. Academic teams have done this for C and Java. The problem is that implementations have many details, so it doesn't scale beyond small programs.
> When I get some time I will look into it further.
I'd say that the effort to learn TLA+ is comparable to learning a very simple programming language with a couple of deep concepts. Scheme maybe. It takes two weeks to be able to write large, complex specifications (though probably longer for the theory to become intuitive). The entire documentation for all the "standard libraries" fits on a single page. The reference for all the language, with full explanations, fits on 4 pages. This is all of TLA+, including the standard library, minus the proof language, including all syntax sugar: http://research.microsoft.com/en-us/um/people/lamport/tla/su... (e.g. all the special syntax for sequences and records is just sugar for functions, so r.f is sugar for as r["f"]). Personally, I'm interested in theory for intellectual reasons, but the single reason I picked TLA+ is that Amazon technical report, where they showed that 1. learning it is easy for engineers to do on their own, and 2. it scales well for very large systems.
I said “formally”, not “with types”. I firmly believe in using the right tool for the job, and some things are best handled with manual proofs. As helpful as types might be for computer-generated proofs (type inference), I'd rather carry out my manual proofs using good old-fashioned predicate logic. Some proof techniques still need to be backed up by type structure, though (e.g., induction over datatypes).
> Every other program in every other languages has most of its meaning expressed informally, in the mind of the programmer.
Unfortunately, I can't read minds. I can only read proofs that have been explicitly written down.
> Unless you believe that no programs work, then nearly all programs that do express most of their meaning informally.
My definition of “work” is “works in all cases”. No bugs. No unforeseen cases.
That's the same sense in which Neel means it.
I agree with you on this one. What actually exists in computing is procedures, which may or may not compute functions. For instance, even in Haskell, so-called “functions” may call `error` or diverge.
However, it's very useful to treat extensionally equal procedures (considering both their effects and their final results) as equal, even if they're syntactically different. This is the basis for compiler optimizations. And the lambda calculus (suitably extended with effectful computations) is better equipped than any machine model to make this identification.
(OTOH, the lambda calculus is a grossly inadequate foundation for concurrency, which is about communication, rather than computation. The main solution I've seen proposed by proponents of functional languages, namely, abusing callCC to get something like cooperative concurrency, is very, very, very bad.)
> Interpreting a computation as one computing functions on the natural numbers or any other set is an entirely interpretive activity that is external to the computation itself.
In practice, people care about the meaning they ascribe to the symbols with which they compute. We use symbols to denote. A meaningless symbol might as well never have been computed at all.
You can't free yourself from thinking in terms of languages :) Not a single one of the machine models -- TM, RAM, neural networks, DNA, digital circuits, quantum computers -- has a concept of a procedure. Procedures are language constructs. Whether you choose to compile Pascal or Haskell to x86 machine code is up to you, but in either case there would be a complexity price to pay.
Machine models take bits and they compute bits, period. Like an apple that falls, they just do they're thing. If a person then wants to say, hmm, that apple's path describes an integral of acceleration, or I will assign the input and output bits mathematical objects, and say that the mapping is a function -- they're welcome to do it, but it's not what the computation does.
> A meaningless symbol might as well never have been computed at all.
Everyone agrees on that. But an apple that falls without Newton to grasp its meaning still falls, and a machine still computes. For meaning you have to pay real, measurable complexity. It therefore doesn't make any sense to compare a model that pays that price with one that doesn't.
Now would I want to. Why would I deprive myself of the benefits of compositionality, separation of concerns, or simply modeling the problem domain as faithfully as possible?
> For meaning you have to pay real, measurable complexity.
Complexity in the sense of complexity theory? I don't see how. If you mean the computational cost of type checking, that's in practice a non-problem as long as the type system is reasonable. (By which I mean: Types are first-order and there is no type-level computation beyond synonym expansion, so plain first-order unification can reconstruct out all the types. Damas-Milner is a special case of this.)
Or are you talking about complexity in some other sense? I don't see the requirement of making sense as a burden. I'd feel burdened if I had to deal with some random computation I found in the wild, with no indication regarding what its meaning is.
But now you're saying that you are interested in programming. TOC is about something else.
> Complexity in the sense of complexity theory?
Yes.
> that's in practice a non-problem as long as the type system is reasonable.
Whether that's an issue for the questions you're interested in asking doesn't define what "in practice" means. It certainly matters for the questions TOC is asking. A model that requires a computationally powerful collaborator -- a programmer -- can't arise spontaneously in nature, for example.
> I don't see the requirement of making sense as a burden.
Again, burden is a question of meaning (proof: you need an agent for something to be a burden for). The requirement, however, shows that the different models are objectively, essentially and radically different.
If you're trying to argue that “computation” is a physical phenomenon in the same sense gravity or electromagnetism are, I have bad news for you: it isn't. The theory of computation, just like information theory and probability theory, is first and foremost a mathematical theory: It is a priori only constrained by the requirement to be logically consistent. This is very different to what happens with a theory of gravitation or electromagnetism, which has to match external observations.
> > Complexity in the sense of complexity theory?
> Yes.
Elaborate.
> Whether that's an issue for the questions you're interested in asking doesn't define what "in practice" means.
In practice, when I submit a Standard ML program to a REPL, the REPL tells me almost instantly whether my program is typable or not.
> Again, burden is a question of meaning (proof: you need an agent for something to be a burden for). The requirement, however, shows that the different models are objectively, essentially and radically different.
Agreed. Only one of the theories is actually useful. (Urgh, it's not a model in the logician's sense!)
Don't know what you mean by "in the same sense", but Turing, von Neumann, Gödel and Hartmanis would have been saddened by your news because they thought (I guess Hartmanis still does) differently. So did Church. The very idea of algorithms -- as Church writes in his review of Turing's paper -- contains a notion of physical realizability. The idea of un/decidability -- only intuitively touched upon in Church's paper, and pretty thoroughly discussed in Turing's -- is predicated on the notion that a computational step takes at least some constant amount of physical time. It is true that a computation isn't a specific physical phenomenon like gravity, but a general, abstract phenomenon, that can be realized in different ways. But if it can't be realized, then it isn't considered computation, unless the people discussing it exclaim very clearly that they're discussing hypothetical computation.
Some people take it further and say that not only computation is physical, but as it is meant to model the work of the mathematician, it grounds all of math in the physical along with it, and things that can't be feasibly computed (in some reasonable amount of time) should be left outside the realm of math. You may have heard this story by Harvey Friedman about the ultrafinitist Alexander Esenin-Volpin who attended his lecture[1], and Paul Cockshott from the Univeristy of Glasgow writes this[2]:
> Turing starts a philosophical tradition of grounding mathematics on the material and hence ultimately on what can be allowed by the laws of physics. The truth of mathematics become truths like those of any other science — statements about sets of possible configurations of matter. So the truths of arithmetic are predictions about the behaviour of actual physical calculating systems, whether these be children with chalks and slates or microprocessors. In this view it makes no more sense to view mathematical abstractions as Platonic ideals than it does to posit the existence of ideal doors and cups of which actual doors and cups are partial manifestations. Mathematics then becomes a technology of modeling one part of the material world with another.
As to the rest, there's much more to computation than programming, and your personal line of work is not the definition of utility.
[1]: https://en.wikipedia.org/wiki/Alexander_Esenin-Volpin#Mathem...
[2]: http://blogs.nature.com/soapboxscience/2012/06/20/turing-the...
I don't see how. That inherent complexity is precisely that computed by the machine (provided that you're talking about a function in the ordinary, set theory sense, rather than in the type theory sense, in which case a function is a set-theoretic functions plus a proof of set membership).
> and of course, you also turn around and favor certain interpretations over others based on the cost of embedding them in your favorite computation model
No, the complexity of evaluation differs in the different models by a small factor (polynomial at most), that is much smaller than the complexity differences of the representation. There is no room for (significant) interpretation here: the typed formalisms can perform computations of possibly arbitrary complexity during their validation stage. They aim prove something and proving something comes at a cost. There is no interpretation by which proving a possibly complex theorem is considered of having little complexity.
The same function may be computed by different procedures with different complexity.
> rather than in the type theory sense, in which case a function is a set-theoretic functions plus a proof of set membership
Not all types denote sets.
> There is no room for (significant) interpretation here: the typed formalisms can perform computations of possibly arbitrary complexity during their validation stage.
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).
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.
How does this even make sense? The whole point to specifying something abstractly is that you want to denote anything that satisfies the specification. And what proof are you talking about? Are you confusing “proof” with “typing derivation”? A single term may admit multiple typing derivations.
> First, the computational complexity of verifying a program is the same no matter when it's done.
You're assuming that you can write correct programs, without taking verification into consideration right from the beginning. This assumption is incorrect.
I am not confusing anything. Again, this is a matter of overloaded terms. When a typed language expression to compute a function Nat -> EvenNat is given, there are two computations that must be carried out: First, a proof that the function yields an even natural is computed (you call that type checking); second (that's the evaluation step), the actual computation is carried out, and an element in the set of even numbers is computed.
When you want to start counting operation is up to you. You can declare that the validation (type checking) phase is not counted. But the fact remains that if you know something -- i.e. that the result of the computation is a member of a certain set -- that knowledge must be gained at some computational cost. If you know it, then it means that something has paid that cost.
> You're assuming that you can write correct programs, without taking verification into consideration right from the beginning. This assumption is incorrect.
I am not assuming anything. When to do something is a practical, engineering concern. It is obviously of extreme importance. But from a theoretical point of view, the total computational effort required to prove a property of a program is the same (given the same conditions), no matter when it is carried out. Of course, engineering concerns move that complexity around between different machines -- the computer and the human programmer -- based on their respective strengths, but the total work is always the same. Just as to sort an array there's a minimum complexity required (O(n log n)) no matter how you do it, so too does writing and proving a program correct has an inherent complexity that has to be paid no matter what.
As stated above, not all types denote sets. For instance, in a language with general recursion, (simple) types denote domains, not sets.
> But from a theoretical point of view, the total computational effort required to prove a property of a program is the same (given the same conditions), no matter when it is carried out.
You are ignoring two things:
(0) There is no magical way to implement the correct program if you don't have verification in mind right from the start. You will implement the wrong program, then attempt to fix it, then have another wrong program, then attempt to fix it, etc. That too has a computational cost.
(1) When you design your program upfront with verification in mind, you actually have a different mathematical object than when you don't. (Just like 2 as a member of the naturals is a completely different mathematical object from 2 as a member of the reals.) If your program design is split into modules (as it should be, if your program is large enough), then enforcing abstraction barriers across module boundaries constrains the size of the design space, often dramatically. (e.g., there are too many non-parametric total functions of type `forall a. a -> a` to even form a set, but there is only one parametric such total function: the identity function.) You note that verified properties could be thrown away after the verification is done, but why would anyone in their right mind want to?
No, I'm not. I'm talking about math. (If you read my comment history, my distaste for “engineering” should be obvious, at least if by “engineering” we mean “software engineering”.)
> but theoretically a building would be just as strong if it were somehow built from the top down.
The amount of mental gymnastics required to produce this statement (not to mention expect someone else to believe it) completely baffles me.
> Computational processes in a living cell, for example, also have to ensure correctness -- and therefore spend computational resources on "verification" -- yet they don't use symbolic logic for that task.
Nature doesn't do “verification”, because there's no specification in the first place. Nature just evolves a variety of systems, and those that aren't fit enough to survive, well, just die. Also, the evolution of biological systems happens way too slowly to use it as inspiration for how to design computational systems for our own purposes.
Good. In that case, verifying that a program conforms to spec in the general case is of as much computational complexity no matter when it's carried out. This is proven and well known. For an overview, you can see my post here: http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...
In short, the reason for that is that the every computational problem with a computable upper bound on complexity can be efficiently reduced to verification. The complexity required to verify is a function of the spec, and can be made arbitrarily hard.
> The amount of mental gymnastics required to produce this statement (not to mention expect someone else to believe it) completely baffles me.
OK, so let me use another analogy. That you can wind up a wind-up toy before I enter the room doesn't mean that just because you hid that from me, the toy requires any less external energy to run than when you'd wind it at any other time. Discussions of ergonomic ways to wind the toy (with a larger lever perhaps) may be interesting, but they're separate from this basic fact.
Verification is a computational problem, and one of a certain complexity. That complexity must be paid, no matter what, no matter when. The knowledge that a certain program has a certain property has a price-tag, and there are no discounts. Because all computational problems efficiently reduce to verification, if you believe you've found a loophole, I could use it to solve much bigger problems than ensuring that your recipe application is correct.
> Nature doesn't do “verification”, because there's no specification in the first place. Nature just evolves a variety of systems, and those that aren't fit enough to survive, well, just die.
You're wrong because, again, you're blind to computational complexity and to computational processes that aren't man-made programs. What you described is precisely how nature computes. That things that aren't fit enough to survive "just die" is a verification process by a genetic algorithm (that requires tremendous time and space complexity) to conform with the spec for genes -- i.e. life's "software" -- which is: reproduce.
Computational complexity results are used in the study of biological systems. Look at the work by Leslie Valiant (Turing award) or Stuart Kauffman (https://en.wikipedia.org/wiki/Stuart_Kauffman). Incidentally, TLA+ can also be used to model systems such as metabolic pathways, as those are very easily described as nondeterministic state machines: http://www.cosbi.eu/research/publications?pdf=5437
> Also, the evolution of biological systems happens way too slowly to use it as inspiration for how to design computational systems for our own purposes.
Maybe, but TOC doesn't study how to design computational systems for our own purposes. It's pure science. If its discoveries turn out to be useful, then that's a happy coincidence.
For that matter, neither does most of TOP for the past couple of decades or so. If you do math to study a system designed for use by a computationally-complex collaborator (the programmer in this case), you must study the collaborator as well. TOP shows no interest in such empirical study, and has therefore been utterly unable to prove that the approaches it advocates actually help write very large complex software systems; indeed it has been even unwilling to test this hypothesis, not even once.
Then, as Dijkstra said, don't focus on the general case: “So, instead of trying to devise methods for establishing the correctness of arbitrary, given programs, we are now looking for the subclass of "intellectually manageable programs", which can be understood and for which we can justify without excessive amounts of reasoning our belief in their proper operation under all circumstances.” https://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/E...
> The knowledge that a certain program has a certain property has a price-tag, and there are no discounts.
So what? If you're designing programs out of reusable components and you don't throw away their proofs of correctness, then much of the cost has already been paid by someone else before you even start.
> You're wrong because, again, you're blind to computational complexity and to computational processes that aren't man-made programs. What you described is precisely how nature computes. That things that aren't fit enough to survive "just die" is a verification process by a genetic algorithm (that requires tremendous time and space complexity) to conform with the spec for genes -- i.e. life's "software" -- which is: reproduce.
This still doesn't make sense. No biological system is “correct” in any meaningful sense. Correctness is always relative to a specification, and, even if your specification is as vague as “survive”, what's happening in nature is that some life forms are lucky enough to be fit for their current circumstances, not all possible ones.
Exactly, except that since Dijkstra gave that talk (early seventies) we have learned some important results in computational complexity. The bottom line is that we know that it is impossible to create a generally useful programming language (even not Turing-complete; even a finite-state machine) where every program is relatively cheap to verify (in 2000 it was proven that language abstractions can't significantly reduce verification cost even though it would have been reasonable to believe that they could; that result is discussed in my linked post). Whatever language is chosen, only a small subset of programs written in that language will be verifiable. Identifying that subset requires extensive empirical research. This is done in the software verification community; unfortunately the PL community is reluctant to conduct empirical research.
> much of the cost has already been paid by someone else before you even start.
Not true. See the Schnoebelen results quoted in my post that I linked to. Composing proofs of program correctness requires proof effort that is intractable in the complexity of each component, not in the number of components. This was proven in 2005. In technical terms, verification isn't Fixed-Parameter Tractable, or FPT, a relatively modern[1] complexity class created to incorporate problems that are intractable in the general case but may be tractable in practice. In simple terms, that each of your components has been proven correct still means that the difficulty of proving the composite's correctness is an intractable function (exponential at least) in the complexity of each component. Of course, theoretically it's better than nothing, but not by enough.
> is that some life forms are lucky enough to be fit for their current circumstances, not all possible ones.
That is only if you view each life form as the computational system. However, that genetic algorithm I was referring to is conducted by all living systems as a single computational system.
You're still focusing on arbitrary programs. Just don't write arbitrary programs. Let your intended proof tell you what program you need to write.
> Composing proofs of program correctness requires proof effort that is intractable in the complexity of each component, not in the number of components.
So keep each component small.
> However, that genetic algorithm I was referring to is conducted by all living systems as a single computational system.
This is still not verification. It's just testing on a much larger scale.
Of course, but easier said than done. In other words, we haven't figured out how to do this yet. So far, the cost of proof exceeds what we're willing to pay for what needs proving. OTOH, researchers often focus not on the programs we need to write, but on the properties they can prove (searching under the lamppost, so to speak); this is the best way of getting results. Some of them then try to convince themselves and others that the properties they can prove of the programs they can prove them on are really those that need proving, and that the cost is affordable. Sadly, this wish hasn't been shown to be true just yet.
Look, I suggest that you try to write a large-scale formally verified program. Forget large; small and non-trivial will do. And I don't mean "verified" as in it type-checks in Haskell, because the Haskell type system can only prove extremely weak properties, but actually verified with respect to interesting logical properties. There is a reason why no one in the history of computing has never come close to achieving such a feat. Interestingly, you find that it is the people who actually do formal verification (you can watch talks by Xavier Leroy, who comes to verification from the PLT direction, or statements made by the people who worked on seL4) are usually the ones most restrained in discussing its possibilities. It can work, depending on what exactly you want to do, but requires a great investment, and end-to-end verification is possible only on very small programs (like seL4 or CompCert) and only at a prohibitive cost, that makes the process worth it only for a handful of very special projects.
Let me put it another way: so far, practice has shown to be very much in line with the difficulties predicted by the theory. Even Schnoebelen says, when discussing the result that language abstractions don't help, that, while true for the worst-case, "has been observed in many instances, ranging from reachability problems to equivalence problems, and can now be called an empirical fact"
Personally, I do formal verification extensively on large projects (much larger than CompCert or seL4), but I don't even attempt end-to-end or manual deductive proof because the cost of those becomes very clear very fast once you start trying these things on big systems. These observations have been reported, AFAIK, by every single industry or research unit that carries out significant software verification efforts.
Formal verification can and does work. But in order for it to work, you need to approach it humbly and know the limitations. Also, you need to know where best to spend your efforts, which is a bit of an art. When you do, you discover that maybe you've not found a way to consistently churn out bug-free programs, but that the quality of your programs has improved considerably.
Just to give you a taste of program proof, this is a simple exercise by Leslie Lamport:
Consider N processes numbered from 0 through N-1, in which each process i executes
x[i] := 1;
y[i] := x[(i-1) mod N]
If you can produce a machine-checked proof of this 2-line program that has no loops or recursion in under one hour, hats off to you. The difficulty of the problem grows super-linearly with the size of the code. People writing real programs, even those intended for verification, write programs that are several orders of magnitude more complex than this toy example.
> This is still not verification. It's just testing on a much larger scale.
It's verification (by an algorithm that is not common in software). The cost of verification comes from the knowledge you wish to obtain, not how you obtain it. Computational complexity doesn't care if you know something by proving it using FOL and natural deduction, dependent types, or by exhaustively trying each input. BTW, as far as the theory is concerned, a test is verification of a more specific property (e.g., the property that your program, when given input x, would, say emit output y followed by output z).
This is exactly what I'm doing: a library of data structures and algorithms, where the verification effort is suitably split between the language and me. The language (in this case, Standard ML) ensures that abstract types can only be used abstractly, and I prove (using paper and pen) that the implementations of these abstract types are correct. A primary concern is simplicity, so if a module has too many invariants to manually prove, it is a natural candidate for splitting into smaller modules.
I'm not saying that Standard ML is the ideal language for this kind of thing, e.g., some limited form of dependent typing would be very helpful (as long as it doesn't compromise type inference), but it's much better than anything else I have tried (including Haskell).
> Do you know what that invariant is?
The invariant to maintain is “there exists some distinguished index i such that x[i] is written by process i before it is read by process (i+1) mod N”. If N = 1, then i = 0. If N = N' + 1, consider some valid interleaving of N' processes, with distinguished index i', and then consider the effect of interleaving one more process.
> The cost of verification comes from the knowledge you wish to obtain, not how you obtain it.
In this case, what I wish to ascertain is whether a living organism is fit to survive in a range of circumstances, most of which will never actually happen.
> BTW, as far as the theory is concerned, a test is verification of a more specific property (e.g., the property that your program, when given input x, would, say emit output y followed by output z).
Tests can verify atomic propositions. They can't verify that a predicate holds for all inhabitants of an infinite set.
That's excellent, but I didn't say "program" for nothing. Programs are usually interactive, with temporal components. But if data structures are your thing, try writing and verifying, say a concurrent R-Tree.
> The only invariant I can see is that “y[i] has been assigned to” implies “x[i] has been assigned to”. From this, we can see that “all y[i]s have been assigned to” implies “all x[i]s have been assigned to”. But this doesn't involve any induction on N so far.
Your reasoning is OK, but it shows how much you're thinking in terms of the language rather than more abstractly. It's also not enough to prove the property.
The crucial state here is the hidden state in the program counter. The induction is not on the number of processes, but on the steps of the algorithm. Each step executes one line of one process (chosen nondeterministically). The invariant, expressed in TLA+ is:
Inv ≜ (∀ p ∈ 0..N-1 : Done(p)) ⇒ ∃ p ∈ 0..N-1 : y[p] = 1 \* (1)
∧ ∀ p ∈ 0..N-1 : pc[p] ≠ "L1" ⇒ x[p] = 1 \* (2)
(2): this is the inductive bit; `pc` models the program counter
This is instantly verified with a model checker. A machine-checked proof is about 60 lines long (I try to avoid formal proofs as they are extremely laborious, but I guess that a more experinced machine-prover than me could do it shorter).
> Tests can verify atomic propositions. They can't verify that a predicate holds for all inhabitants of an infinite set.
Exactly, and each of those atomic propositions has a cost of verification. Moreover, we can prove (again, it's in my post) that we can't in general generalize from one input to another, so the cost of verification over an infinite number of inputs is infinite in the general case. Of course, it can be done in practice, but we can tell exactly how hard that would be: the cost of verification is proportional to the number of states in the algorithm -- the minimal algorithm that satisfies the full spec; not necessarily your actual program. Properties that are easily checked by simple type systems like those of Haskell and SML can always be satisfied by much simpler programs (in fact, a FSM or, if polymorphic recursion is used, then a PDA).
Errr, yes, you're right. I noticed I messed up after I posted my comment, then edited it accordingly. I don't see why I need to perform induction on the program counter, though.
I posit that, no matter how you interleave your processes, there is some distinguished index i such that x[i] is written by process i before it is read by process `(i+1) mod N`. To prove this, I use induction on N:
(0) If N = 1, then i = 0.
(1) If N = M + 1, inductively assume that we have a collection of M processes with distinguished index i. Now consider the effect of adding one more process, respecting the interleaving of the original processes:
(1.a) If the new process is added at any index other than `i+1`, then the original processes i and `(i+1) mod M` still have contiguous indices in the new collection, and the former still writes to the common variable before the latter reads it.
(1.b) If the new process is added at index `i+1`, then at least one of the two following things must happen:
(1.b.i) The original process i writes to x[i] before the new process reads it.
(1.b.ii) The new process writes to x[i+1] before the original process `(i+1) mod M` (now `(i+2) mod N`) reads it.
No analysis of the program counter was required, and as a result we get a far more beautiful proof. You used a sledgehammer, I used a sculptor's chisel.
> Properties that are easily checked by simple type systems like those of Haskell and SML can always be satisfied by much simpler programs (in fact, a FSM or, if polymorphic recursion is used, then a PDA).
I never claimed that I could delegate the entirety of the formal verification task to a type system like that of Haskell or SML. And, to be honest, I don't even think using computers to verify everything is such a good idea. What I want is automation for the boring and repetitive parts (the vast majority), so that I can concentrate exclusively on the hard ones. (Which isn't to say that I'm happy with the little amount of work Damas-Milner does for me. It's possible to do much better, without sacrificing automation.)
This is not true. At no point in your induction is it proven that it is always the last process that writes x before the first reads it, nor is it necessarily the case.
> then at least one of the two following things must happen:
This, too, is untrue. The events may occur in the precise opposite order. If this were true, then it would have been an invariant that either process N-1 or process 0 would necessarily write 1, but this is not the case.
> No analysis of the program counter was required, and as a result we get a far more beautiful proof. You used a sledgehammer, I used a sculptor's chisel.
Excellent, except that my "sledgehammer" is a proof technique that's been proven complete, i.e. if a program property is provable, it is provable via an inductive invariance, which is amenable to mechanical proof checking (and, indeed, I mechanically checked it in TLA+). Good luck getting your proof (which is called "behavioral") -- even if it were correct -- to verify formally.
Chord is a distributed algorithm that was published in 2001 and quickly became popular. It got thousands of citations and plenty of industry implementations. In 2011 it even won a "test of time award". Its authors said, "Three features that distinguish Chord from many peer-to-peer lookup protocols are its simplicity, provable correctness, and provable performance". They, of course, provided proofs. However, in 2012, Pamela Zave, using a model checker, showed that "of the seven properties claimed invariant of the original version, not one is actually an invariant". The point is that when algorithms are concerned, "proofs" are often not proofs.
See: https://brooker.co.za/blog/2014/03/08/model-checking.html and https://www.youtube.com/watch?v=iCRqE59VXT0
> I never claimed that I could delegate the entirety of the formal verification task to a type system like that of Haskell or SML.
Just to be sure: proof with pen and paper isn't formal verification. It is pretty the very definition of informal verification. Formal proof means using natural deduction or sequent calculus. This is too hard, so a machine-checked proof is acceptable. But any proof or any other kind of verification not carried out or verified by a computer is not formal.
I didn't say anything about “the last process”, though. I just took a collection of M processes, with some valid interleaving, and inserted one more process, at whatever index j, displacing all pre-existing proceses j...M-1 one place to the right.
>> then at least one of the two following things must happen:
> The events may occur in the precise opposite order.
Let A and B be processes with adjacent indices (for my purposes, M-1 and 0 are considered “adjacent”), such that A's write happens before B's read. If we insert a new process C in between A and B, then A and B no longer manipulate a shared variable, but instead A writes to a variable C reads, and C writes to a variable B reads. Then at least one of the two following things must be true:
(0) A's write happens before C's read.
(1) C's write happens before B's read.
This follows from these facts:
(0) A's write must happen before B's read.
(1) C's write must happen before C's read.
Was that too hard to understand? If it was, you need to relearn to prove things by hand.
> Just to be sure: proof with pen and paper isn't formal verification. It is pretty the very definition of informal verification.
While the proof I gave above is most certainly informal, you can prove things formally using pen and paper. The formality comes from the use of explicitly given deduction rules, not from the use of a computer.
Of course. Sorry. For some reason my mind read i as N. It was late at night... I'm convinced the proof follows from your invariant, but the inductive step is a bit tricky, as i is not the same for every interleaving. My proof is simpler, as the invariant holds for -- and more importantly, maintained by -- every step made by the system, and there's no need to consider various interleavings. It also doesn't require induction on N.
> The formality comes from the use of explicitly given deduction rules, not from the use of a computer.
That's true and I said as much, but doing so is extremely laborious. Do you actually use natural deduction?
Ah, the joys of nondeterminism! It gives “there exists” an, ahem, “interesting” meaning. This is why I only do imperative and concurrent programming when it's absolutely necessary (e.g., when no functional and deterministic program could be asymptotically as efficient).
> My proof is simpler, as the invariant holds for -- and more importantly, maintained by -- every step made by the system
My invariant is prettier. It doesn't need to be maintained “throughout the computation”, because it's a static assertion about the program: “regardless of the interleaving of operations, there exists some i such that...” Almost invariably, the program is a much simpler mathematical object than the computations it gives rise to. Dijkstra noted “that our intellectual powers are rather geared to master static relations and that our powers to visualize processes evolving in time are relatively poorly developed.” https://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/E...
> It also doesn't require induction on N.
Induction on the program counter is even harder! The inductive case of my proof doesn't even look at the entire computation: it looks at most at three processes at a time. It's literally less work than what you propose.
> Do you actually use natural deduction?
In the design of type systems, yes. If I want to prove something by hand, hell no. Natural deduction is much nicer to prove things about than it is to prove things in.
In TLA+ nondeterminism is as natural and graceful as determinism (it's a matter of ∨ vs ∧), and the functional concepts of parameterization and function types are just special cases. Nondeterminism is what allows refinement relations. You have it whenever you have types, but the language you use just doesn't use the same words to describe it.
> because it's a static assertion about the program
Mine is as static and as global as yours (and has the benefit of being easily verifiable mechanically)! You're just not trained to see it. You've been told that concurrency and imperative constructs are "dynamic" and are hard to reason about. That's just because FP is bad at reasoning about them, and prefers syntactic decomposition. There is nothing dynamic about a proper, pure description of what to you seems a messy dynamic process. The entire program is just a single, pure semantically unambiguous first-order predicate.
I had a discussion about this with a PLT person once, and he kept asking how you prove static properties in TLA+. It took me a while to understand what he meant, as "static" vs. "dynamic" are necessary when you want to reason about syntax. In simple logic, there's just a single formula.
> Almost invariably, the program is a much simpler mathematical object than the computations it gives rise to
You don't reason about each computation, but about what you'd call the "program", which in TLA+ is called the algorithm, as not to unnecessarily confuse with ideas that are related to syntax. The algorithm is just a boolean predicate, and my proof is that that predicate implies another (which implies the property).
Now when I look at how FP people reason about code I wonder why they have to complicate things so much. Sequential, concurrent, parallel, nondeterministic, deterministic, algorithms, properties -- they can all be reduced to a single first-order predicate, with the simple implication relation proving anything you want to know about any of them (that the program satisfies a property or a "type", that the deterministic program is a refinement of the nondeterministic one, that the parallel program computes the same result as the sequential one, that the sequential program has a worst-case complexity of such-and0such), all with simple, familiar logic and semantics that fit on a single page.
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. Distinguishing a class of computations that can be expressed as functional programs is distinguishing a class of computations whose meaning can be established with simpler tools, and thus obviously a beneficial activity.
> There is nothing dynamic about a proper, pure description of what to you seems a messy dynamic process. The entire program is just a single, pure semantically unambiguous first-order predicate.
Last time I checked, imperative programs don't denote first-order predicates, but rather predicate transformers. Quite different things. A predicate transformer is a higher-order mathematical object that relates two (possibly first-order) predicates - a precondition and a postcondition.
> You don't reason about each computation, but about what you'd call the "program", which in TLA+ is called the algorithm, as not to unnecessarily confuse with ideas that are related to syntax.
Your use of induction on the program counter reveals that you're just using the program as a proxy for a class of computations.
> The algorithm is just a boolean predicate,
Um, no. Predicates don't express computation.
> and my proof is that that predicate implies another (which implies the property).
Would you have been able to produce your proof entirely by yourself? That is, unaided by a computer. I produced my proof using nothing other than my brain.
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? How do I hide the representational choices of a module whose internal implementation I'm not currently concerned with?
> 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
First-order logic is not “high-school math”. You can't expect most high schoolers to know how to correctly manipulate logical quantifiers. (Of course, a competent programmer should know, but that doesn't mean one should force themselves to use a more complicated tool when a simpler one is available.) And axiomatic set theories (such as ZF), which are built on top of first-order logic, are definitely not “high-school math”. Have you ever seen the crazy things that Harvey Friedman does with large cardinals?
> plus three temporal operators, of which only one is really used for safety properties).
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.
> In TLA+ there is no such thing as an imperative or a functional program. (...) E.g., in TLA+, all algorithms (...) denote a set of behaviors, where each behavior is an infinite sequence of states.
Then in TLA+ all algorithms are expressed as imperative programs.
> Think of algorithms as abstract state machines, and reasoning becomes -- if not simple -- then as simple as possible (today, at least).
By virtue of exploring large state spaces?
> But the proof works on the representation of the program, which is just a logical predicate.
Which is it?
(0) Two programs that compute the same result, but have different efficiency characteristics, are represented as logically (not just syntactically) different predicates.
(1) You don't distinguish between programs that compute the same result, but have different efficiency characteristics.
The former is unusable as a basis for reasoning about extensional equality. The latter is unusable as a basis for reasoning about complexity.
> Yes. First I thought of it, then I wrote it, then I added details until it checked.
Checked by whom?
> 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.
I don't disagree with this one.
> But, unfortunately, proof assistants don't help you uncover a proof. Model checkers can do that sometimes.
Type inference reconstructs type derivations all of the time. Reliably. Of course, those type derivations are all boring routine, but it means that human programmers themselves aren't burdened with it.
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.
Set theory doesn't have any facilities for data abstraction. If anything, it's the antithesis of data abstraction: 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.
> TLA+ has a simple module system.
Hierarchical modules? Parameterized module families? Multiple views of the same module, showing or hiding different aspects of it? I use this stuff everyday not only to keep my programs modular, but also to keep their proofs of correctness modular.
>> 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.
You were the one who originally brought up ZF, describing it as “high-school math”, so I was just refuting that.
> 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+.
If elegance is your only criterion, it's very hard to beat Martin-Löf type theory. Of course, usability matters too, and there MLTT fails miserably, at least for programming purposes. Higher-order dependent types don't come for free.
> It's done reliably because the properties they represent are kept very computationally simple.
That's a feature. It helps you delimit the routine stuff (and can be reliably verified mechanically, and should be most of your program, if it's designed sensibly) from what requires creativity to prove.
That being said, of course, existing type systems don't automatically verify everything that could be considered “routine”, so this is an area where further improvement is necessary.
> The problem is with more interesting propositions.
Prove them by hand. Good old-fashioned brain usage is never going away.
---
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?
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
Inv ≜ PartialCorrectness
∧ ∀ p ∈ ProcSet : pc[p] ≠ "Line1" ⇒ x[p] = 1
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
> 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.
So it doesn't scale to entire programs?
> A 3000 line spec (over multiple modules) is considered very big.
A 3000 line program is fairly small.
> Come on. That people write PhDs on algorithms they implement in Python
Presumably they don't actually prove things about Python programs directly. If they do, what formal semantics for Python are they using?
> doesn't mean that Python isn't a high-school-appropriate language.
Formally reasoning about Python programs is a huge pain. Why would anyone want to subject high-schoolers to that?
> Informally, it goes as follows. (proof)
Okay, it was much shorter and sweeter than I expected. Well done.
> TLA+ comes with a model checker. You just press a button and if your assumptions are incorrect you get a counterexample.
What I want is proofs, not just truth values. A proof is a syntactic object that can be analyzed, partially reused, combined with other proofs, etc.
TLA+ is not a programming language. A 3000 line spec easily specifies a 100KLOC program.
> What I want is proofs, not just truth values. A proof is a syntactic object that can be analyzed, partially reused, combined with other proofs, etc.
Sure, but: 1. if you're wrong, a model checker gives you a counterexample; this is invaluable in understanding what's going on and fixing your bugs. It's much easier to prove something when it's true. 2. Unfortunately, the difference between the cost of deductive proof and running a model checker is at least one if not two orders of magnitude. It is common industry experience (reported most recently by Amazon about TLA+), that a model checker provides the best bang-for-the-buck. It actually reduces development costs overall. Deductive proofs are cost-prohibitive for all but the most well-funded, patient and rather modestly sized programs. They're worth it mostly if you're willing to pay 10x to go from, say, 97% certainty to 99.9%.
So, which is it?
(0) After you verify a TLA+ specification, you still have the rather large task of making sure your actual program satisfies the specification. In this case, why should I bother verifying something that isn't the final program?
(1) The program can be generated from the specification. In this case, the TLA+ specification is a program, although it's written in an unusually high-level language.
> Deductive proofs are cost-prohibitive for all but the most well-funded, patient and rather modestly sized programs.
It would be a lot more cost-effective if we used languages, libraries and even operating systems geared towards formal verification.
Theoretically, you can verify the program itself in TLA+, in a manner similar to how seL4 verified their code. You compile your final code to TLA+ to produce a low-level spec that captures the actual semantics of your progam, and check that it is a refinement of your high-level spec. Research teams have done this for Java and C (http://tla2014.loria.fr/slides/methni.pdf). The problem is that it doesn't scale, and neither does any other form of end-to-end proof. Humanity has never been able to formally prove an actual program that is anywhere near what we would call "large".
The reason you'd bother doing it is that 1. unlike end-to-end verification it is not only affordable, but also reduces costs, and 2. it actually works in uncovering the most costly problems, as verified by years of experience in industry on large projects.
> The program can be generated from the specification.
Ah, that is an interesting research question. Obviously in some cases a program could be generated. The spec would need to be deterministic for one (or nondeterministic in a way that makes sense for an actual program, like when representing multiple processes), computable (you can easily specify a program that takes an arbitrary program as input and says, "in the first step, let x be equal to TRUE if the input program terminates on the input 13, and FALSE otherwise"), and pretty low level because you can easily write things that would be extremely inefficient to run (like "let x be the smallest prime that's the sum of three squares" or something). Lamport believes that it may be possible (for a properly amenable spec) using machine learning. But it's not like compiling any high-level programming language.
> It would be a lot more cost-effective if we used languages, libraries and even operating systems geared towards formal verification.
Research doesn't seem to indicate that it would be, or rather, even if it is a lot more cost effective, it is still beyond affordable for all but high-assurance software, and high-assurance software already makes use of such languages (SCADE and SPARK work very well). But even in high-assurance, the industry doesn't bother with deductive proofs, as model checkers are automatic and work where they're most needed (SCADE) and SMT solvers are also reported to be effective for very restrictive languages (SPARK, but I've never tried it). Manual deductive proofs are used sparingly, to tie together results from automatic verification processes: http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.h...
And we probably never will. AFAICT, our only hope is to build large software out of small components that can only be composed in obviously correct ways, so that the bulk of the verification effort is spent on each individual component, rather than on their interactions (a hopeless task). This is reflected in my ML programming style: A function exported by a module must not impose any preconditions on its argument that can't be enforced by the module itself. On the other hand, at a higher-level, a functor (parameterized module) may impose nontrivial preconditions on its argument.
> Lamport believes that it may be possible (for a properly amenable spec) using machine learning.
That is extremely unpalatable to me. I'm more than perfectly willing to use a different formalism (like TLA+, although I'd like better integration with actual programming languages), but not to resort to massive trial and error (which is what machine learning ultimately boils down to) to generate programs.
---
Anyway. What I can take from this whole discussion is:
(0) As your original blog post says, there are two ways to look at computation. One view simply pays attention to the physically realizable aspects of computation: nature certainly doesn't care that I want to use bits (or more generally, symbols from a finite alphabet) to represent values from a problem domain, or that this bit means one thing but that bit means another thing. The other view pays attention to how computation can be structured and given useful meanings: the (non-C) programmer in general doesn't care that the same bit pattern can be used to represent different values of different types.
(1) If I may use a physical analogy, writing purely functional programs and using equational reasoning on program terms as the basis for verification are akin to trying to solve every physics problem by appeal to conservation laws. The two main drawbacks of this approach are that not every physical system is conservative (we want effects, for which monads provide a solution) and that it's useless for reasoning about time (for which there is no solution).
(2) On the other hand, the verification style you advocate, by looking directly at state transitions, is akin to solving physics problems by appealing to the laws of motion, suitably expressed as differential equations. The two main drawbacks of this approach is that it may require lengthier computations (which is less of a problem if the computations can be delegated to a computer) and that it doesn't gracefully handle computations whose state is split across several modules, none of which should inspect the state of the others (for which AFAICT there is no solution).
(3) Do we have an equivalent of Lagrangian or Hamiltonian mechanics, to be able to relate both styles?
But Schnoebelen's theorem proves this is impossible. (in my post: http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...)
The post also has an example of that: the foo/bar program, AKA Goldbach's program. bar is correct (i.e., it correctly decides whether its parameter is a prime -- maybe there's a bug in my implementation, but we can assume it's correct). This leaves foo. The first two lines are trivial. This leaves the next three lines (I guess that in Haskell it would be one line). I don't see how you can get more modular and composable than that! And yet, we haven't been able to prove the behavior of those three lines for 300 years, even though they're nothing but a simple decrementing for-loop, a single subtraction operation and a single disjunction! Why? Because bar (i.e. `prime?`), in spite of being correct, has a very complex behavior; it can be reasoned in some contexts, but not in this one.
In any event, every attempted project decomposed the problem as much as possible. The task still proved prohibitively expensive (although maybe not for high-assurance development!).
> The other view pays attention to how computation can be structured and given useful meanings
Almost, but not exactly. The values in machines matter greatly to the machine. The language models are human centric, i.e., they compute with values that matter to humans. But the important point of the post is that the two views are incomparable, as the second requires significantly higher work, i.e., expressing a computation in a way that's meaningful to humans is in itself a significant computational effort.
>and that it's useless for reasoning about time (for which there is no solution).
And that it doesn't work on real world systems. You can reason equationally about the gravity equation all you like, and compose as many instances as you like. But that wouldn't help you to decide interesting properties.
> On the other hand, the verification style you advocate, by looking directly at state transitions
I don't have an aesthetic reason to advocate this style. I'm a pragmatist, so I chose it and advocate it because it is the only style that has so far proven to work. That you can pick it up in a week or two instead of six months, and that it supports automated tools that make verification affordable are also great pragmatic advantages. If you show me another one that works as well on real-world systems, I'll be happy to use it.
> and that it doesn't gracefully handle computations whose state is split across several modules, none of which should inspect the state of the others
I'm not sure how you get that. TLA+ handles composition very nicely. There are operators that specifically hide variables, called temporal existential quantification. The formula basically says, "there exists a behavior over these (hidden) state variables, such that those other (observable) variables satisfy X".
> Do we have an equivalent of Lagrangian or Hamiltonian mechanics, to be able to relate both styles?
That's above my pay-grade, but TLA can be embedded in FP (in fact, the standard Isabelle distribution contains an embedding of TLA+, as TLA+ uses Isabelle as a backend prover, and I think there are embedings in Coq, too[1]), and FP can be embedded in TLA by conisdering extensional equality only. It's mostly a matter of convenience, possibly for different classes of problems.
The thing is that deductive proofs of any kind so far seem untenable in all but extreme circumstances. The problem with approaches that rely on types (and this may be orthogonal to FP, maybe not) to prove interesting logical properties are more rigid, and less able to accommodate more partial forms of verification. Maybe there's work on that, though. As a result of that, the TLA approach (in a general sense) is simply more battle tested, and with better real-world results.
[1]: http://ucsd-pl.github.io/veridrone/papers/memocode2015.pdf
This is an astonishing claim. Can you formulate measure theory in TLA+?
2. I am not a logician so I don't know of the formal particulars of measure theory, of any limitation ZFC has in formulating it, or of any TLA+ specific limitations in that regard. However, TLA+ is not a general proof assistant (it can certainly be used to prove general math theorems, it just wasn't designed for that task), but a language for specifying and reasoning about algorithms and large software systems. In that, it is as powerful as Coq.
3. There are completeness proofs for TLA, i.e., that anything that you can state about a computation, you can state in TLA, and anything you can prove about a computation you can prove in TLA. Now, this isn't quite accurate: TLA is a linear temporal logic, and there are some things that you can state and prove in a branching-time temporal logics that you can't in a linear logic, nevertheless, as Moshe Vardi says in Branching vs. Linear Time: Final Showdown[1], it makes more sense to prefer linear time logic because empirical evidence suggests that it's far more useful. There is one glaring downside: TLA is unable to reason about probabilistic algorithms[2]. However, it is possible to embed reasoning about computation in the + part of TLA (i.e. ZFC) and reason about probabilistic algorithms in that way, and I assume that this is how it would be done in Coq, too. So you could do everything in TLA+ without the TLA bit, but that would be inconvenient, as the natural representation of algorithms in TLA is especially convenient and the main justification for the approach. So I would be very interested in seeing an extension of TLA meant to deal with probabilistic algorithms.
4. In the end, what matters isn't theoretical strength (by which Coq and TLA+ are equivalent in anything that concerns algorithms), but convenience. I am sure that there are some problems that are easier to formulate and reason in Coq than in TLA+. But the fact that no one has ever used Coq for a large software system, and that the handful of use cases in industry were always done in cooperation with academic experts while TLA+ is used in very large projects by "plain" developers speaks volumes to the strength of the approach.
[1]: https://www.cs.rice.edu/~vardi/papers/etaps01-ver13.pdf
[2]: You can describe any probabilistic algorithm in TLA (i.e., state that an algorithm performs a certain step with a certain profitability). What you can't do is then state a probabilistic theorem about that algorithm, as "in 70% of the cases, the algorithm gives the right answer".
Sure, algorithms are mathematical and much of mathematics can be recast as algorithmic, but still they have quite a different flavour. If a tool designed to help with one is actually the best tool to to help with the other, then that is astonishing.
I don't think it's better, but it is as mathematically powerful, certainly when within the realms of ordinary math. As it is not designed for this task, I would assume that Coq would be more convenient.
Coq is a full decade older than TLA+ (and Lamport mentions Coq when he discusses the design of TLA+ as something to avoid because of the arcane, virtually unknown math; even the TLA logic is 5 years younger than Coq), and even Coq isn't the first theorem prover, nor the most popular. It wasn't even designed to be the "best" math prover, but (I would imagine) to be a tool for type theorists to see how well how their ideas work. After all, Isabelle (which preceded Coq and serves as a TLAPS backend) is very good at "general" logic (not type theory).
BTW, TLA+'s proof languages looks very different from Coq, and is declarative in nature. It is based on Lamport's "how to write a proof", and, as I understand, Isabelle's Isar is also inspired by that style[1], so TLAPS looks a lot more like Isar.
Also, remember that the very concept of machine-checked formal proofs of mathematical theorems are currently used mostly by people who design those provers and hobbyists. Few mathematicians are keen on the approach (although I think they should be). Proof of software correctness, OTOH, is something that a larger group is interested in.
But back to my main claim: TLA+ lets you express specifications about a program that are as rich as anything Coq would let you do. It was designed by people who are experts in software specification rather than by type-theorists. I would guess that Coq may be a better for some things (maybe proving general theorems about some classes of programs), but when it comes to actually reasoning about large software in the industry, TLA+ and its older kin (Z, B-method and more) are almost the only game in town. Isabelle is also ahead of Coq in verifying real-world systems.
[1]: http://isabelle.in.tum.de/Isar/isar-thesis-Isabelle2002.pdf
Very suprised to hear this from someone who wrote this very article on the nature of computation!
Verification is hard. We all agree. But that is for the worst case. Alternatively we can say that it is hard to verify arbitrary programs. I am utterly unconvinced that it is hard to verify programs that are designed to be verified, and I am utterly unconvinced that it is hard to design programs to be verified.
How should I convince myself that it is hard either (1) to verify even programs that are specifically designed to be verified, or (2) to write such programs?
(I don't mean hard in practice, I mean in theory.)
Didn't we discuss that issue on Reddit? Anyway, as the complexity of verification is proportional to the number of states. If you write the program from scratch, the number of states is dictated by your spec (as every computational problem, every function has an inherent computational complexity). Your spec can be arbitrarily hard.
Now, it's not a matter of worst-case. That writing and verifying arbitrary programs is the very same problem is easy to see: given a program A, and a property I wish to verify P, I then create a spec S = A ∧ P, i.e, the program you write must behave like this arbitrary program and satisfy P. So there is no difference between writing from scratch or verifying. Indeed, you can see that static analysis tools can often prove on arbitrary programs the very same properties that are enforced by type systems.
Of course, not every algorithm and property are worst-case, regardless of whether the program is being written or given. There are useful classes of programs/properties that are easier to verify, and the language can make useful restrictions. So far, examples that work well in practice are SPARK and SCADE. Each forbids memory allocation, including unrestricted stack growth.
I don't follow. What has A got to do with it? I am given a spec P. You claim that it's hard to write a program that satisfies P, pretty much regardless of what P is. I don't see how A is relevant at all.
If you want another example of how a spec can be hard, consider this one: "write a program that for every input n, an even integer greater than two, outputs the smaller of two primes whose sum is n". Do you think writing that program and proving it correct is any easier than verifying the 10-liner in my post?
Or even this: "write a program that sorts a list of integers". You know for a fact that that program has a minimal time complexity of O(n lg n). That complexity, in turn, partly determines how hard it will be proving the program correct. You know that it will be easier than "write a program that returns the first element of its input list", whose time complexity is O(1) (actually the difficulty of verification is more related to the space complexity, because the space complexity is a better approximation of the number of states the algorithm must have in order to solve the problem, unless the algorithm can be a pushdown automaton).
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?
I have absolutely no idea. The entire focus of my software development philosophy for a decade or has been to make programs easier for humans to understand, not easier to write proofs about (although there's some overlap). I do wonder how big the weak but extremely useful class of properties (like Rust's memory safety) is.
> almost all (92%) of the catastrophic system failures are the result of incorrect handling of non-fatal errors explicitly signaled in software.
The exception-handling code is there, it's just that no thought has been put into it. They say that their simple linting tool could have detected and prevented a good portion of those very costly bugs.
Really? What's so special about strings? Perhaps I want computations to consume and produce trees. It seems like you've picked an arbitrary setting for computation and said "Look! My constructions which are naturally suited to this setting are naturally suited to this setting!".
So there's a real difference between various configurations of gas molecules in a box, and a real difference in the computational cost of representing them. Your statement is not unlike saying, "oh, so you've picked a high-entropy configuration, how convenient! What's so special about high entropy?" High entropy and low entropy aren't symmetrical. It takes more energy to move in one direction than the other.
Again, you shouldn't be surprised by this at all (I'd think it's rather obvious). Since typed formulations do proof work in their validation step (that can be Turing-complete in some cases), obviously that means that there is more complexity in their representation, otherwise, you'd have computation for free.
You can choose whatever representations you like. But representations that express more information, come at a higher computational cost.
I'm not sure why you think that I'm surprised, or even why you think that I disagree with your overall argument. I'm just trying to help you build your argument by pointing out the most obvious aspects which need more careful elucidation.
So your claim is that in the physical world strings are more fundamental than trees. Good to know. In fact I think there's an even simpler reason than the one you give of "entropy". That is, trees require space which grows exponentially in their depth, and thus they can't even be represented in the physical world.
A string is quite different from a stream. A string is typically considered random access, for a start.
On Scott's blog Neel talked about functions '(unit -> bool) -> (unit -> bool) -> bool', but this example seems spurious. He asserted that Turing Machines could receive the arguments Godel encoded but the Lambda Calculus couldn't. I don't see why. If you also let the Lambda Calculus receive its arguments Godel encoded then it can inspect them and perform the same dovetailing that the Turing Machine would.
Do you know of a more compelling example?
I never said the Church-Turing thesis fails. I only said that it only claims what it claims.
> He asserted that Turing Machines could receive the arguments Gödel encoded but the Lambda Calculus couldn't. I don't see why.
In the lambda calculus, if you have the Gödel number of a Turing machine, you can simulate that Turing machine. But if you have a lambda abstraction, you can't produce the Gödel number of a Turing machine that computes the same (partial) function as the lambda abstraction. The only thing you can do with a lambda abstraction is apply it.
Internally, in the lambda calculus itself, or a model of it, there are two caveats, however:
(0) Nothing guarantees that all internal inhabitants of a type are denotable by external pieces of syntax. For example, most real numbers are undefinable. (There are only countably many formulas over a finite alphabet, but uncountably many real numbers, ergo, most real numbers can't be “pinned down” using a formula. That doesn't prevent them from existing. The situation is exactly the same with a type like `nat -> nat`.)
(1) The right internal notion of equality isn't syntactic equality (which doesn't even make sense, for the reason stated above), but extensional equality.
If all of this sounds too strange, read more about model theory, Gödel's completeness theorem, and the Löwenheim-Skolem theorems.
Undefinable real numbers exist, whether you can compute them or not.
> and we are talking of models of computation.
A theory of computation that rejects the existence of things that can't be computed is like a logic that rejects the existence of FALSE because it can't be proved. Where does the busy beaver function sit in your conceptual model?
I agree with you, but as you probably know this is a deep ontological question. The meaning of something "existing" has been debated for many centuries, especially for cases such as this.
> A theory of computation that rejects the existence of things that can't be computed is like a logic that rejects the existence of FALSE because it can't be proved. Where does the busy beaver function sit in your conceptual model?
There is a difference between rejecting and classifying. I am not proposing a new computational model. Turing's model classifies the busy beaver function as non-computable. Correct?
I thought we were discussing Church-Turing. This assumes Turing Machines, and what they can compute. Of course you can break everything by assuming an imaginary machine that can compute functions that are not computable by Turing Machines...
Yep.
> I thought we were discussing Church-Turing. This assumes Turing Machines, and what they can compute. Of course you can break everything by assuming an imaginary machine that can compute functions that are not computable by Turing Machines...
Turing never redefined the concept of “countable”, which belongs in set theory. If you had asked him what the cardinality is of the set of functions from the naturals to the naturals, he would've answered you “uncountable, of course”.
This seems trivial to prove: any function representable in any given programming language maps to a finite string of characters, and finite strings of characters maps to natural numbers.
EDIT: In fact I'd guess any function type A -> B where A is infinite cannot be mapped to the naturals.