Hacker News new | past | comments | ask | show | jobs | submit login

> The Church-Turing thesis is a statement about which functions of type `nat -> nat` are computable, either in the lambda calculus or using Turing machines.

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.




How then do you state the Church-Turing thesis? I note that the Wikipedia page claims that Church and Turing themselves used the word "function":

https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis#S...


They do use the word function, just not in terms of the language itself, but in the same sense of saying that a falling apple integrates the function from its mass to acceleration; it's a human interpretation of the encoding. I would state the Church-Turing thesis like so: a universal computation model can compute anything any physical machine can. As Hodges says in one of the links in the article, this is how Church and Turing themselves understood it. How would I define "anything"? As a function on any countable set -- the natural numbers, would do -- and I would explain what it mean to compute a function: pick a function, pick an input element, pick a finite representation for the input and output; if a physical machine can compute the output representation from the input representation, so can a universal computation model.

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.


a function between any two countable sets, e.g. (Nat -> Nat) -> (Nat -> Nat): pick a representation for the input and output

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 you take the normal mathematical definition of a function as a mapping from one set to another, pick two sets, pick a representation and all models can compute the same mapped elements. Tell me what your (higher-order) function is — i.e., what output element it maps to what input element — and a TM would compute the exact same outputs. That it can’t internally “reason” about those functions is obvious, but, as I showed, that ability comes at a cost. You could build, say, a Haskell compiler that would pay that cost and translate the language to a machine representation (or, speaking more abstractly, a TM could simulate, say, System Fω — at a computational cost), or you can use an abstract language model without any underlying machine, but the same cost must be paid regardless.

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.


> and solves a harder problem than necessary to compute that function in the normal set-theory sense

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.


> People who use set theory as their foundations...

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.


Of course, proving things, that is, doing mathematics requires work. But at least it's work that produces a useful result, unlike carrying out computations without paying attention to their meaning. (By the way, this meaning always exists, even if you don't particularly care about it.) And the best moment to study the meaning of a computation, in the sense of minimizing the amount of long-term work, is as early as possible, which is exactly what types force you to do.


But this is now a programming discussion, not a computation discussion. Also, I don't think it's right to declare things "useful" only if they're useful to the particular problems you're trying to solve.

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.


> Also, I don't think it's right to declare things "useful" only if they're useful to the particular problems you're trying to solve.

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.


> Pray tell, what's the use of a computation without paying attention to its 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.


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

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.


> Please suggest alternatives - that actually work.

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.


> AFAIK, the only languages that fully express the com meaning formally with types are the dependently typed ones.

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.


So you're specifying an empty set. There has never been a large program that's been completely formally proven -- not a single one -- and there are therefore no methods that work. The small programs that have been mostly proven, took such a great effort, that their creators wouldn't say that the approach "works" in any widely applicable way.


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


> > Which tool satisfies the following criteria? ...

> 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).


Well, the 1994 paper does have about 2500 citations:

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


> there's no need for 500 tutorials on monads

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?


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

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

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

Here's how things become easier:

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

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

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

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

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

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

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


> What doesn't work is a specification language that's also a programming language.

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?


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

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

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

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

> Correctness does compose in my experience as a mathematician

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

> Please explain your terminology.

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

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

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

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

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

> What does it mean to you?

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

> What exactly does that mean?

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

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

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


> 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

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.


> That's not an assumption I want to have to make!

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.


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


> They do use the word function, just not in terms of the language itself, but in the same sense of saying that a falling apple integrates the function from its mass to acceleration

That's the same sense in which Neel means it.


No, he doesn't. In the type view, the computation is asked to do two things: compute the output and check a proof that the output belongs to a set. Each of these questions has its own computational complexity. You may say that the first question comes from free by deciding how to think of the apple; the second certainly doesn't.

See also https://news.ycombinator.com/item?id=12403508


Yes he does. If by "Which functions nat -> nat are computable" he meant "functions written in some typed language" then the answer is vacuously "all of them".


Not all functions of type nat -> nat are computable in any formalism. You can write plenty of programs that are really of type nat -> nat in say, Haskell, that try to compute a non-computable natural function. They just can't do it and they'll never terminate for some inputs. But they're still perfectly well-formed.


> From the TOC perspective, there is no such thing as functions at all.

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.


> What actually exists in computing is procedures

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.


> You can't free yourself from thinking in terms of languages

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.


> 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 closely as possible?

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.


> But now you're saying that you are interested in programming. TOC is about something else. (...) A model that requires a computationally powerful collaborator -- a programmer -- can't arise spontaneously in nature, for example.

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!)


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

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


The notion of a function having any inherent complexity is rather at odds with your earlier assertion that putting any sort of meaning on the result of running a Turing machine is strictly human interpretation rather than a hard fact of computation (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).


> The notion of a function having any inherent complexity is rather at odds with your earlier assertion that putting any sort of meaning on the result of running a Turing machine is strictly human interpretation rather than a hard fact of computation

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.


> I don't see how. That inherent complexity is precisely that computed by the machine

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 same function may be computed by different procedures with different complexity.

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

> Not all types denote sets

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

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

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


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

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.


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

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.


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

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?


Again, you're talking about engineering. That's great, but I'm talking about theory. You're saying that it's easier to build a building from the bottom upwards -- and that's true -- but theoretically a building would be just as strong if it were somehow built from the top down. Of course, no one would think to build skyscraper starting from the top, but that doesn't mean that the theory of structure must always incorporate the study of construction. I'm not talking about the process of construction, but the properties of the structure. I'm not arguing with any of what you've said here, simply talking about different aspects. Keep in mind that not all computational process -- certainly not all studied in TOC -- are programmed by humans at all. 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. This means that there's value in studying the problem of verification even separately from the study of programming. Indeed, this is how it has mostly been done in academia. The software verification community uses very different concepts from the PLT community, concepts that are much closer to abstract machine models than to language models.


> Again, you're talking about engineering.

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.


> No, I'm not. I'm talking about math.

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.


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

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.


> Then, as Dijkstra said, don't focus on the general case

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.

[1]: https://en.wikipedia.org/wiki/Parameterized_complexity


> Whatever language is chosen, only a small subset of programs written in that language will be verifiable.

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.


> Just don't write arbitrary programs. Let your intended proof tell you what program you need to write.

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]
and stops, where each x[i] initially equals 0. (The reads and writes of each x[i] are assumed to be atomic.) This algorithm satisfies the following property: after every process has stopped, y[i] equals 1 for at least one process i. It is easy to see that the algorithm satisfies this property; the last process i to write y[i] must set it to 1… The algorithm satisfies this property because it maintains an inductive invariant. Do you know what that invariant is?

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).


> Look, I suggest that you simply try to write a large-scale formally verified program. 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.

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.


> a library of data structures and algorithms

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)
(1): this is the simple property invariant

(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).


There is still one glaring issue with your thesis that remains unresolved.

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.)


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

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.


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

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.


Yes, but P can be arbitrarily hard to implement. This is hard for you to see, so I'm incorporating A into P just as an example of how we can make the spec hard. If it were easy to write programs that conform to arbitrary specifications, it would have been just as easy to verify arbitrary programs, because I can reduce the latter to the former by making the arbitrary program the spec of the new one.

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).


Sure, I know that there are some specifications P that are hard to implement (and some that are impossible!). What's not clear to me is whether the specifications we care about implementing in practice are hard to implement.


In practice it's obvious that they're hard! Look at the bugs people make and look at the effort required for seL4/CompCert (both are fairly simple systems).

Isn't the computation done with logical cells represented by a composition of boolean functions? And which are synthesized via functions sometimes from a functional language? What does this say about idea that, at ISA or abstract level, you're just doing computation if it's implemented as boolean, state machines.

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.


Turing personally addressed the question of analog computation and determined that they add nothing over discrete machines, as discrete computers can compute anything an analog computer would do to the desired precision that matters to you. He even discussed the subject in his 1936 paper, when he introduced his model. He wrote that eventually one would need to distinguish between two states, and so a model where states can be arbitrarily indistinguishable adds nothing, so you may as well discretize. When he wrote about the operation of the brain he said that it shouldn't matter if the brain is continuous or discrete; its operation could be simulated to arbitrary precision by a discrete process. He did wonder about quantum effects, though (he understood quantum entanglement when he was 16, Hodges writes).


> Computations consume and produce strings.

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!".


Like entropy, computational/informational content is absolute. Strings have higher entropy. If I say, "I'll hand you a piece of fruit", that statement objectively has less information (and therefore smaller computational complexity to verify), then if I said, "I'll hand you an apple". A tree really is inherently more complex than a string. It's like an RNA molecule being more likely to be naturally synthesized in the primordial soup than, say, a cat. Of course, an unspecified "tree" could be as "entropic" as an unspecified string, but my guess is that you mean something more specific.

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.


> Again, you shouldn't be surprised by this at all (I'd think it's rather obvious).

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.


I gave a more specific explanation in another comment: trees are more complex because they require nodes to be connected and each node to have no more than one parent. A string is any stream of measurements. The exponential growth of trees doesn't bother me, because you can have a natural encoding that doesn't grow exponentially, and doesn't increase interpretation cost exponentially.


And I gave a more specific objection there too.

A string is quite different from a stream. A string is typically considered random access, for a start.


But isn't a computation that consumes and produces strings a function String -> String? (Or perhaps ordered_set<String> -> ordered_set<String>?)

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




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: