Hacker News new | past | comments | ask | show | jobs | submit login
On Two Views of Computation in Computer Science (pressron.wordpress.com)
107 points by pron on Aug 31, 2016 | hide | past | web | favorite | 187 comments



> You’re free to think about computation as acting on bits… but for those bits to do us any good, they have to actually represent something (e.g., data structures).

I suspect this is a case of confusing epistemology with ontology.

Galaxies are ontologically composite in that they're the highest holonym in the supervenience hierarchy [0]. Atoms are ontologically fundamental in that they're the the lowest meronym in the supervenience heirarchy.

Galaxies are epistemically abstract in that the notion of galaxy is far removed from everyday experience. Atoms are also epistemically abstract in that the notion of atoms are also far removed from everyday experience. What's epistemically fundamental are the immediate objects of our everyday experience, like chairs and food. (My impression of Zen is that it advises to focus more on things like chairs and food [1].)

https://www.xkcd.com/435/

In the xkcd, which is more "fundamental", Math or Economics? Well, it depends. Likewise, what's more "fundamental", bits or ADT's? Well, it depends.

[0] powers of 10: https://www.youtube.com/watch?v=0fKBhvDjuy0

[1] http://www.itsokblog.com/2011/01/wash-your-bowl-zen-of-mothe...


Well, in this case all models are quite abstract, and there's a very real computational complexity difference between them. The key, if I were to use your way of presenting the issue, is the recognition that some epistemological abstractions are more computationally costly than others. So it's true that you can choose either representation as a foundation, but the representations objectively and radically differ in their computational complexity.


The key is to recognize how it's not just that TOP and TOC both measure X with different models. It's that TOP measures X while TOC measures Y.

It's as if we claimed Spell Checking were as complex as Natural Language Processing because they were both called "linguistics". Yes, they both abstract over language. But the primitives of Spell Checking are glyphs while the primitives of NLP are morphemes. Glyphs don't exhibit the same patterns as morphemes. Which is why Spell Checking uses a Trie while NLP uses a Matrix. Debating whether glyphs or morphemes are "more fundamental" is a distraction.

Likewise, bits don't follow the same patterns as ADT's. Calling both the study of bits and the study of ADT's "Complexity Analysis" is misleading, which I believe is what Pressler was getting at. But we've put bits and ADT's in the same bucket for the entire history of computing, because the Church Turing thesis (i.e. anything a TM can do, lambdas can do too) lead us to believe Turing and Church were studying the same primitives.


What I was getting at in the article is that:

1. TOC and TOP ask different questions.

2. The disparity of the computational complexity involved in the two classes of models is so great, that it is objective proof that they represent two distinctly different things, and therefore comparing them directly is meaningless. That a jet and a bicycle require vastly different amounts of energy to power is conclusive and objective proof that completely different tradeoffs must be involved in choosing them.


I think mathematicians would call this "representation theory." This is the whole question of do we think of a calculation as syntax, or can we represent this syntax as a "dynamic", or action; something that is being moved around or transformed.

Some people really are driven to just calculate stuff (pushing language itself around), and others seem to want to know "what does it mean?" Ie. what are the representations of this language. Logicians call this semantics: it's a model for the syntax.

I'm a theoretical physics grad student, and see plenty of this. Most physicists seem to just want to calculate stuff, and don't care where the symbols "live". For me, a calculation is rarely enlightening. I want the context, the type theory that tells me how the pieces talk to each other.


I don't think mathematicians would use "representation theory" for this, since representation theory is a very specific and precise subfield that is at best tangentially related to the theory of computation.


The point of the article is that different representations incur different computational complexity costs. Those costs are objective and absolute. If two different representations each require wildly different computational complexity, then the two can't be meaningfully compared on the same terms, because the two are clearly and objectively different.


I think you've got an interesting point, and I'd like to add to it a bit and refine/correct it a bit.

First off, minor thing, but as Jeremy has pointed out, your terminology is wrong; "representation theory" means something else. You seem to mean something more like "model theory".

But anyway -- I'm a mathematician, and I've noticed something like this too when I've dealt with physicists or their writings. But before I discuss physicists, let's discuss mathematicians, because I think you've mischaracterized them a little.

(Note, all claims here are just based on my experience.)

You talk about considering syntax vs. considering the different models of the syntax. But most mathematicians, unless they are logicians or set theorists or something, don't take either of those views. They take the Platonic view -- they're discussing a world of mathematical objects; the statements just describe it. They're not considering the statements as primary and then considering multiple models of it, they're considering the one true world of mathematical objects and describing it with statements (which might have other models, but who cares). This point of view breaks down somewhat when you have to deal with things like the continuum hypothesis and such, but that sort of thing doesn't really come up in ordinary mathematics.

(Note though that taking the Platonic view does not necessarily mean taking the "theory of programming" perspective the article discusses. I mean, I wouldn't take Aaronson's view, that computation is prior to everything else; that's pretty incompatible with it. But to my mind, computation is fundamentally about finite strings over a finite alphabet. Talking about computation with higher types -- where the Church-Turing thesis can fail -- as though it were, well, computation, feels really weird to me.)

Also, another terminological correction: Most mathematicans don't care about type theory. They care about types, at least implicitly, though they might not use that term; but they are not going to consider types as an object of study in and of themself. But yes -- when you want to understand a mathematical object, one of the first questions is, "What sort of object is that?" or "What space does that live in?"

So anyway -- yeah, physicists. I've noticed this too, and I don't know what to make of it. Where physicists don't tend to fully specify their, let's call it an ontology, and have a hard time answering questions like "What sort of object is that?" or "So that's a function from what to what?" Where they don't seem to properly distinguish between a mathematical model or description, and a method of calculation that's useful when working with that model or description. (I have so often failed to get an answer to, "So are virtual particles an actual physical phenomenon predicted by the quantum field theory, or are they just part of a useful method of calculation for working with quantum field theory?") Where they seem to care primarily about methods for getting numbers out, rather than building full, coherent models.

It's all weirdly instrumentalist, which to me seems backwards from what you'd expect -- like, mathematical Platonism is a philosophical question, but the physical world is definitely real! And sure, maybe the bits we can't measure are more of a philosophical question too -- especially since one can quite possibly come up with multiple isomorphic usable models for the laws of physics, whatever they turn out to be -- but still, mathematicians have no trouble just treating their mathematical objects as real things to be reasoned about, so this kind of instrumentalist view among physicists seems weird to me.

I hadn't even considered the possibility that they were thinking "syntax-first", so to speak! But I guess that does kind of sum it up pretty nicely. Bugs the hell out of me, though. Makes it pretty difficult to talk about the math of their theories with them, too.


> your terminology is wrong; "representation theory" means something else. You seem to mean something more like "model theory".

I really do mean representation theory, in the widest sense of the word. Wide because I am trying to make connections here, not distinctions.

So for instance, of course group representations. On the one hand there is an abstract group multiplication, and on the other side we are representing this as a geometric action.

The same thing goes for "bigger" gadgets, lie algebras, hall algebras, etc. All kind of algebraic objects that we can define abstractly (syntactically) but then lo! it is actually represented by some kind of (geometric?) action.

And then in a more logical vein you have the lattice type theories. Boolean algebras, heyting algebras. These things have topological representations (or is it functions on topological spaces). And then to denotational semantics of lambda calculus. And it's all kind of a syntax on one side, and a semantics on the other.

I don't know much about models of set theory, but I'm assuming these also involve a kind of "active" representation of syntax. I would also include things like algebraic topology, topological quantum field theory. These are all "functors" which act to represent an algebraic gadget in a more dynamic way (i'm possibly over-generalizing here.)

Anyway, there's no concrete definition for what I mean by a "representation" so that's why i gave some examples. It's quite mysterious imho.

> So anyway -- yeah, physicists.

Well, it's easy to criticize physicists, but I also think mathematicians are guilty of this. Ok, so they define their calculations rigorously (not always), but then it's gloves off and away we go! I've come to realize that the whole program of categorification is an attempt to bring more context to these calculations (this is what I would call type theory for mathematics btw.) And most mathematics is written down as calculations, without this context. Probably because it's much harder to categorify everything. The simplest example of what I mean is this: "why keep track of a (finite) set when you can just say how many elements are in the set?" And so on. I really do think that alot of mathematicians are just as guilty as physicists of the "shut up and calculate" attitude. But, they are certainly much more humble :-)


What you're describing sounds more like homology theory, where there is an abstract set of concepts (short exact sequences, etc.) which become different theorems in different contexts. But, unless I'm mistaken, most of the time these are closer to unifying foundations, or starting points, from which the special features of each model allow you to say more beyond the abstract framework. So sure you can get some general category-theoretic theorems, but saying the specific model is useless (as the Language folks say about Turing machines) is ludicrous.


This is an interesting article, but I'm still fairly confused about the notion that is made

>Harper’s attack on the utility of machine models and lack of modularity is tantamount to an architect saying to a chemist, “both of our disciplines concern the arrangement of molecules, yet my discipline is superior, as yours doesn’t even have the modular notion of a room!”

But wouldn't the whole point be that a chemist, seeing the room as nothing less than an abstraction, can also understand the room through their given framework? Much in the same way that, for any computational model, we can think of a TM with an Oracle tape, or some similar IO model, that has the same computational power as any defined language?

I'm afraid that I thought I understood the distinction at first: where those who support CT view computation as a fundamental case (e.g. every other mathematical 'primitive' can be derived from a computation with the appropriate oracles[1]) and and the TOP view which sees mathematical foundations as the main case, and then sees computers as being an abstraction of functions in some sense, such that one can construct a calculus of these functions which constitutes a language.

Did I get this all wrong? I'm afraid I still don't understand the main distinction to be honest. It seems that both parties are going around in circles on exactly the same thing, but assuming different axiomatic systems and showing that each is equivalent to the other.

[1] For example, with no oracles, we receive all of constructive mathematics, etc.


You can translate and transform many things to many others. The important question is what is the computational complexity of the transformation? If it is large, then the two things are very different.

As Scott Aaronson once said, waterfalls could be viewed as playing chess, but as the complexity of the translation from the "waterfall language" to a chess language understandable by humans is as great as the complexity of an actual chess-playing program, all the work is done in the translation.

So the question you should be asking is where the complexity is being spent and on what.


Wait, but I thought the question being posed wasn't about the computational complexity of any model but about the power of a given computational model relative to another (e.g. the subject of the CT thesis).

Even if we're talking about just computational complexity, if we allow Turing machines with arbitrary oracles, or (equivalently) we allow arbitrary mathematical constructions in languages, I'm still unsure as to why the complexity matters.

W.r.t the waterfall case. Sure, I agree with that statement, but I'm unsure as to how it plays into the final case---the question isn't about a specific model performing a specific task, but about a model being able to completely replicate another in terms of computational power. Anything I can do in a language (with some functions) I can do in a Turing machine with the appropriate oracles; and conversely, anything I can do in a Turing machine with some given oracles, I can do in a language.


What I get is that the question is "Does it make any sense to compare the two models, or are they just different things?" and the tentative answer is "They are different things, but one end of TOP coincides with TOC".

I'm fully convinced. Both concepts answer different questions, and that is my favorite test (instead of the OP's "does one model map into the other?").


Both models are equally powerful in the things they compute in terms of the Church-Turing Thesis. The TOP view also has other consideration. My point in the article was not to settle the debate on Aaronson's blog but to show that language models and machine models are objectively and inherently so different from one another that comparing them in terms of programming concepts (like types) is meaningless.


And it seems that most of the "my way is superior to yours" is based on setting up strawmen of "yours" to make it be addressing the same questions as "mine".


Yes, but it goes a little further. I can't say my way is superior to yours if my way means solving a harder task and paying market price for it.

I got the leather seats because I chose to pay full price for them. That they come as a standard option with the car because the car is more expensive is not an argument. You can choose to pay the same difference in price and have them installed in your car, too.

Whether those leather seats matter or not is no longer an objective question but a question of values, and here is where caring about completely different values is the point.


I see, okay; I caught that point in the article through the first part, but the latter part got me stuck back on the same point hence the question. Thank you for the clarification.


>The important question is what is the computational complexity of the transformation?

In my view it makes no sense to use metrics from one model on the other. There is no computational complexity involved in the transformations defined in ToP. This is like measuring the computational complexity of a mathematical proof - it has no complexity, it's delcarative.


> This is like measuring the computational complexity of a mathematical proof - it has no complexity, it's delcarative.

There are few things that are absolute in this universe, but computational complexity is one of them. There is plenty of complexity involved. Have your heard of proof complexity? How do you know that a proof is a proof and how is a proof created? It's pretty much the core of P vs. NP question (and first discussed by Stephen Cook, the same guy who formally framed P vs. NP): https://en.wikipedia.org/wiki/Proof_complexity

Actually, the first one who asked the question of P vs. NP was Kurt Gödel (https://rjlipton.wordpress.com/the-gdel-letter/), and as a mathematician, he was very much interested in the complexity (although he didn't use that word) of proofs. He said that if P = NP (not in those words):

> If there really were a machine with φ(n) ∼ k ⋅ n (or even ∼ k ⋅ n2), this would have consequences of the greatest importance. Namely, it would obviously mean that in spite of the undecidability of the Entscheidungsproblem, the mental work of a mathematician concerning Yes-or-No questions could be completely replaced by a machine.


The author contends in the article's abstract that machine models are "self-contained" whereas "language models" (not clearly defined, but meant to encompass at least an untyped lambda calculus) are not. But both can be viewed as a state plus a well-defined set of rewriting rules, so I suspect that the article is struggling to make what is really a distinction without a difference.


Author here.

> But both can be viewed as a state plus a well-defined set of rewriting rules, so I suspect that the article is struggling to make what is really a distinction without a difference.

1. I state that the untyped lambda calculus is, indeed, a borderline case, and is a simple rewriting system which, in turn, is a special case of a nondeterministic abstract state machine.

2. That many things are abstract state machines does not mean that the computational complexity required to validate whether what you have is a well-formed description is similar.

3. That complexity difference is absolutely huge -- zero for the machine models vs. exponential to undecidable for the typed language models. It is hardly a struggle to draw the conclusion that the two are objectively completely different classes.

Also, I gave a list of machine and language models. The latter group consists of the process calculi and the lambda calculi.


Why is the complexity of parsing well-formed states from strings somehow interesting? If you generalize to trees and pick the right alphabet, suddenly every element of your datatype is a well-formed lambda term.

It's also unclear if you're talking about the complexity of type inference or type checking, what annotations you're allowing, etc. Your claims about complexity re: states of typed languages are too hand-wavy to engage with.

And yet there's still a glaring error: for a very popular machine model, namely the C abstract machine, it's undecidable whether a state is meaningful (regardless of how you set up your parsing problem).

So, you have an interesting idea about the difference between machine models and languages but it clearly doesn't hold together. People have been studying the relationship between machine models and languages for quite some time, and it's relatively well understood. Machine models are one of the many ways to give semantics to languages. They just don't have many useful properties compared to more "abstract" approaches, and are mostly used to reason about implementation.


> If you generalize to trees and pick the right alphabet, suddenly every element of your datatype is a well-formed lambda term.

How would you feed trees to the computation? Also, once types are involved, nothing can help you. I admit that untyped LC is somewhat of a borderline case.

> It's also unclear if you're talking about the complexity of type inference or type checking

Doesn't matter in this case. Pick a string representation -- any representation -- and see if it's well-formed. You can include the types and then only type checking would be necessary, or not -- and then it's type inference. Either way, the complexity is significant.

> namely the C abstract machine

That's not a machine model.

> it's undecidable whether a state is meaningful

The same goes for any language and your definition on "meaningful". You can always say that something meaningful is a little finer-grained than the language can express, or the validating the language itself is also undecidable. Got simple types? Only primes are meaningful.

> They just don't have many useful properties compared to more "abstract" approaches, and are mostly used to reason about implementation.

My point is that they're not comparable. A glass of water doesn't have the same useful properties as a blender, yet they're both made of molecules. However, there's an objective difference: a blender consumes far more energy, so of course you can use that energy to do more things.


> How would you feed trees to the computation

Um, well the computation (can be set up to) proceeed(s) on algebraic datatypes, so this seems trivially easy.


:) You're just pushing the complexity into the validation of the algebraic type.

Look, a typed formalism does extra work of proving the type safety of the input. Checking a proof has a non-negligible complexity. If that cost could be ignored, then I have a computation model that solves NP problems in zero time: it has a type system that requires that the types form a proof certificate for the problem. All (obviously valid) inputs are then trivially reduced to "yes". In fact, you know very well that some type systems are Turing complete. If the complexity of validation is ignored, then those models can compute anything that's computable in zero time.

Types can prove things. The cost of the proof is well known, and is related to the difficulty of the problem. The universe doesn't let computational complexity slide. What, you think that God says, "oh, you clever boy, you chose a typed model so I'll let you have this proof for free!" ?


> You're just pushing the complexity into the validation of the algebraic type.

Who says it needs to be validated, any more than your string needs to be validated?

> The universe doesn't let computational complexity slide. What, you think that God says, "oh, you clever boy, you chose a typed model so I'll let you have this proof for free!" ?

You're responding to something completely unrelated to my statement.

To be clear: I wasn't suggesting a typed lambda calculus.


A tree is still more complex than strings, because it has rules: one parent per node and no cycles. Those need to be validated. But I have absolutely no problem accepting that it is possible to find an encoding of untyped LC which would bring it very close to a TM encoding. This wouldn't be surprising as LC doesn't do more computational work than TM at the validation step (unlike typed formalisms).

I specifically wrote that untyped LC is a borderline case, and it's unclear where precisely we want to draw the line. What is absoutely clear is that System F and TM are essentially, qualitatively and objectively very different, and when people try to compare them, they often, without noticing, describe two different computational problems, with two different complexities.


You're positing some new notion of complexity, without a definition, where lists are somehow fundamentally different than trees. Sorry, but that kind of claim requires more than just just an appeal to intuitions about how they might be implemented on a typical CPU. They're both just initial algebras.

The fact that your grand ideas about machine and language models doesn't apply to the lambda calculus should be a hint. We know how lambda calculus relates to typed languages: it's a degenerate case with a single type. Any differences in the complexity of type-inference or checking are between language models. You can't (without wildly waving your hands) formulate a meaningfully comparable problem for TM states.


> A tree is still more complex than strings, because it has rules: one parent per node and no cycles. Those need to be validated.

Hmm, I'm not convinced that this is sufficient to show that strings are simpler.

After all, a string has rules too: a cell in the string is either at the beginning, or the end, or the middle, and it has neighbours left, right or not at all depending on those conditions, and at most one such neighbour in each direction. Even appeal to the physical world doesn't help. If I have a physical piece of DNA, how do I know it hasn't mutated so that two different strands branch off it and it becomes, essentially, a degenerate tree?

I do think that the thrust of your argument is correct but it's not as clear cut (at least not yet) as you seem to be making out.

> What is absoutely clear is that System F and TM are essentially, qualitatively and objectively very different

Absolutely agreed! If they weren't, I'd be happy writing my day-to-day code in Turing Machines.


You're talking about the graphical representation of a string. A string is any stream of measurements (over time, if you like).

> If they weren't, I'd be happy writing my day-to-day code in Turing Machines.

And if they weren't, we'd see neurons or DNA using type-theory!


Since you seem to have thought about the fine details of this much more than you are letting on here and on your blog post I suggest you post an addendum (or even a new blog post) to be more precise about what exactly they are. There's a lot missing as it stands, and interested readers like myself are left to fill in the blanks.


Could you encode all untyped lambda calculus expressions by just numbering them and writing the number as the string of bits?

Maybe this enumeration is the "external collaborator" in this case, but it's a very simple one.


Inside the lambda calculus, the only thing you can do with a lambda abstraction is apply it.

And one thing you can't do using your numbering scheme (which is basically a Gödel numbering) is establish whether two syntactically different functions are extensionally equal (under some fixed reduction strategy).


You could, but you'd need to spend even more effort before beginning interpretation to turn the number into a form that LC can interpret.


> zero for the machine models

That's absolutely not true. It takes non-zero effort to determine whether the code for a Turing machine actually implements a valid Turing machine.


No,it's actually right. See my post comment answering the same question. It is the circuit models that actually pose a harder challenge, but even if you won't accept my reasonable zero-cost encoding where a misconnected input is interpreted as a constant 0,the cost of validation is still less than even untyped LC.


You state there that "at worst I would need O(n) time" so are you in fact conceding that my claim "It takes non-zero effort to determine whether the code for a Turing machine actually implements a valid Turing machine." was correct?

https://pressron.wordpress.com/2016/08/30/what-we-talk-about...


I gave a natural, reasonable encoding that requires zero validation: every string is a valid TM, and every TM can be easily represented by that encoding and directly executed. However, some may object to the encoding on some grounds, so I said that even the strictest critic would agree to a more complex validation, which is still lower than that of untyped LC. Similarly, I made lenient assumptions about untyped LC (variable shadowing). Without it, you'd need to keep track of every variable that's in scope, so as not to accidentally bind it again. With it, evaluation becomes complex by a bigger factor than a TM becomes under my zero-cost representation.

It's important to understand that encoding is always a tricky subject, because every different encoding requires a different interpreter, and one could ask whether that interpreter is really the "original" TM or "original" LC (of course, there's no argument over huge complexity differences, but slight ones are up for some debate). I think that under very natural, reasonable encodings, the machine models require zero validation; I also think that allowing variable shadowing in LC is reasonable and doesn't completely change the model. It's perfectly OK to disagree with me on this point, but it really doesn't make a difference.

As to providing more detail in the post, well, I don't want to get lost in details that are ultimately inconsequential, and no matter what level of detail you choose, there will always be those who don't find it detailed enough. I prefer the interactive approach of an online discussion.


It’s really weird that the Church-Turing thesis, which is ridiculously robust at first order, falls apart so comprehensively at higher type.

A statement like that makes me feel like Neel Krishnaswami does not understand the Church-Turing thesis at all (what does the Church-Turing thesis even mean at a "higher type"), but considering that this person has significant experience in this field, much more than I do, I am just going to assume that it is me who does not understand until I read up on this exactly.


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 completely disregards:

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


Sorry if I'm missing something fundamental, but (1) shouldn't matter if there's some mapping between a) those types and b) functions of type `nat -> nat`. 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. IOW, whatever transformation it is that the other-typed function makes (edit: or whatever input-output mapping), it is isomorphic to one on `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.


> (1) shouldn't matter if there's some mapping between those types and functions of type `nat -> nat`.

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.


>That's the thing. In some languages, this mapping doesn't always exist.

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!


> The mapping exists, just not necessarily within the language

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.


>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. ... writing a function that inspects the representation of an abstract type isn't “difficult” - it's literally impossible.

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.


> You're right that some languages simply lack certain capabilities, but that's an issue of access, not computation per se.

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 computations 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 the developer has certified as making sense.

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
Such that they compose to identities:

    backward . forward = id :: Foo -> Foo
    forward . backward = id :: Bar -> Bar
I'm pretty sure there's no isomorphism between `nat -> nat` and `forall a. a -> a`. Just to give one example.

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


You genuinely don't know how to write a TM that implements the identity function, or is there some technicality that it fails? If the latter, I'm not sure how it's relevant to my phrasing of the CTT.

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


> You genuinely don't know how to write a TM that implements the identity function, or is there some technicality that it fails?

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.


Whether or not you can map everything in the higher order language to the nat -> nat one is what's at issue, not the reverse.

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.


> Whether or not you can map everything in the higher order language to the nat -> nat one is what's at issue

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.


You would only not be able to map higher order functions to Gödel codes if it is not the case that for some n, f(n) outputs but does not determine m. I'm far from the most knowledgeable programmer in the world... but I do know that such a function could not be implemented by a computer.

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.


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

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


Computers in the real world pass all their time evaluating functions from nat -> nat. It is programmers that use different types.


Computers in the real world pass all their time executing the instructions that programmers give them. (Okay, not true, they pass most of their time waiting for I/O to complete, or simply doing nothing.) If a linguistic abstraction prevents you from giving certain classes of wrong instructions, that's very useful, even if the abstraction has no runtime manifestation.


> If a linguistic abstraction prevents you from giving certain classes of wrong instructions, that's very useful, even if the abstraction has no runtime manifestation.

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


> But notice that this applies to programmers, not computers.

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


As far as the computer is concerned, it is running a nat -> nat function over some data you passed it, and displaying the result.

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 the computer is concerned, a program is just a list of instructions. Not even functions of type `nat -> nat` exist at that level. However, that isn't a very convenient way to program, which is why high-level programming languages exist.

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.


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


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


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.


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


Regarding (1), can you give a compelling higher-order example for which Church-Turing fails?

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?


> Regarding (1), can you give a compelling higher-order example for which Church-Turing fails?

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.


Does a type exist such that it cannot be mapped to the set of natural numbers?


Sure, in Haskell 'IO ()' cannot be mapped to the set of natural numbers (within the language).

EDIT: In fact I'd guess any function type A -> B where A is infinite cannot be mapped to the naturals.


You mean mapped one-to-one? Depends on your model of computation. For example, in the simply typed lambda calculus, equipped with a natural number type, as well as structural recursion on it (but not general recursion), `nat` and `nat -> nat` aren't isomorphic types.


Humm... But the set of Turing Machines is countably infinite, and a nat -> nat function is necessarily representable as a Turing Machine.


Externally, in the metalanguage, you can count syntactically distinct terms, and, of course, the collection of terms that have type `nat -> nat` is countable.

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.


Yes but the real number that cannot be pinned down using a formula can also not be pinned down using a computation, and we are talking of models of computation.


> Yes but the real number that cannot be pinned down using a formula can also not be pinned down using a computation,

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?


> Undefinable real numbers exist, whether you can compute them or not.

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


> Turing's model classifies the busy beaver function as non-computable. Correct?

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


It is not necessarily representable. By diagonalization, in fact, nat -> nat can be shown to be uncountably infinite. Intuitively, an example nat -> nat function that is uncomputable is ~Ld, the function that, given a natural index i into the diagonal of the table of Turing machines and their accepted strings, returns the opposite of whether machine i accepts string i. The output is then clearly equal to no Turing machine, since it differs in at least one position. In order to encode this function, an oracle is required. As such, nat -> nat uncountability can be shown to be central to proving Turing recognizability.


Ok, that's a good point, but it is also true that functions requiring an oracle cannot also be represented in any Turing-complete programming language, right?

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.


Well,

Another factor is that Church-Turing "at first order" isn't a mathematical theorem - (notice "thesis", not theorem).

The thesis is that all determinant computation is equivalent to Turing machines and lambda calculus (which are each computable with each other). This is a hypothesis about the physical world (or the "imaginable" world).

Thus Church-Turing is very significant - but not necessarily mathematically significant, as a mathematical theory, it's taken as the equivalence of Turing machines and Church's recursive functions (but that's just a theorem which only suggests the (nonmathematical) thesis.

The thing is, a lot of mathematicians are much more enamored of the mathematical world than the physical world. For an enthusiastic mathematician playing with high order recursive functions, a generalization of the Church-Turing theorem seems much cooler than the statement about the physical world that the Church-Turing thesis implies.


I'm not really sure I completely understand where the conflict is here. Even in the "machine model" the church-turing thesis "fails spectacularly" once you start adding in unreasonable things like halting oracles. TM+Halting oracle > TM. It's just that the TM+halting oracle doesn't exist in our universe, even though you can define it mathematically.

When building a language, it's similarly easy to introduce "unreasonable" things that either require huge complexity to translate to the machine representation or might even be completely unrealizable in the real world! Even ignoring higher types, compiling a C++ program requires a potentially unbounded amount of work because templates are a turing-complete functional programming language. As stated in the article, just determining if a C++ program is valid is undecidable!

Nothing stops you from designing these languages, but you can't say that Church-Turing fails until you consider also the systems required to actually execute these languages in the real world. If you can't, then your programming language is perhaps an interesting mathematical abstraction, but just as useful ultimately as that TM+halting oracle model of computation.


> TM+Halting oracle > TM

Why is this a failure of the Church-Turing thesis? The Church-Turing thesis says, "Anything that can be computed in our reality (i.e. by a human, ignoring resource constraints) can be computed by a TM." TM+Halting oracle doesn't satisfy the hypothesis.


It's not a failure of Church-Turing. The whole point of my comment is that you can easy construct more powerful models that are "unreasonable" because they don't exist in our universe. It's the same for programming language models.


The article refers to one quora answer where the author says - "The machine-based models offer no notion of composition of programs from parts". The instructions are the parts of the so called machine model, isn't sequencing of those instructions and control flow instructions are nothing but composition?


It's a very impoverished form of composition if the only things you can really compose are the absolute primitives, rather than allowing you to compose things that are themselves composed. When you "program" with Turing machines, you don't have a way to take a section of "code" and paste it into another, larger program. You'll have to deal with two pieces numbering their states the same, overwriting each other's tape data, etc. If you have two Turing machines that solve separate pieces of the problem, you know there exists a single machine that does both things, but nobody actually goes and constructs that machine. Instead, they just mention its existence as justification for writing "do this; do that;" in a higher-level machine description.


I think the problem can be defined as "Composition without isolation", each composed sequence of instruction has this same global context (all of memory) to work with which can lead to problems.


What he means is that complicated programs can be built from simple parts. In programming languages you can just take simple parts and compose them into a single program.

If the simple parts are given by machines, then in general there is no canonical way of composing them into a machine for the composed program. You have to construct a new machine from the machines for the parts. An example is the sequential composition of two functions with logarithmic space usage. You cannot just use run one machine after the other, but you have to modify both machines and then build a new machine that contains them in the right way.

Of course, one may use systematic constructions to combine simple machines into more complicated ones. But this amounts to the implementation of a programming model.


I think you are confusing the word machine in this context. It is not the usual general purpose word machine that people use in every day life to denote a physical system. The word machine in context of model of computation means a specific type of "formal system" to describe computation. The problem of composition is about how this formal system does or doesn't support it.


No, I do mean formal machines like Turing Machines. Sequential composition of logarithmic space Turing Machines is a standard example for lack of compositionality.


Honestly,

I think Aaronson is clearly and transparently correct about Church-Turing and higher types. Computation on higher types is just a higher-order construct having no more to do with computation as we understand it than other higher order constructs like Hilbert Spaces.


Academia is feudal and thus no answer to this is about to become widely accepted. :(


Actually it's a bit more like 42.


How is showing that two representations are fundamentally different because they objectively and radically differ in computational complexity open to interpretation?


It shouldn't be.

I'm skeptical of your parsing argument because the normal way to construct type theory terms is inductively in their "native" tree form, which is cheap. Looking at them as a formal language isn't so convenient.

As a PLer, I hope dependently typed langauges see wide use not because they are the one true foundation of everything, but because they are the richest lingua franca for every academic discipline to represent their ideas—I'm personally enamored of such theories as a foundation for math, but I don't know much about the theory of computation and I'm fine if others just see it as a tool.

Anyways once that happens and fields have distilled their intentions into precise models in the lingua franca, perhaps the walls between fields can be broken down and we finally grok each other's concepts.


> their "native" tree form, which is cheap

It is not cheap at all, as type checking can be arbitrarily hard, depending on the type system, and perform arbitrary computation at the "validation" stage. This is real, significant (and useful, depending on circumstance) computational work, that no formalism or representation can reduce (only hide, by pushing it over to the collaborator).

> but because they are the richest lingua franca for every academic discipline to represent their ideas

I disagree. I strongly recommend you (and everyone) read this terrific essay by Lamport on a lingua franca for algorithms: http://research.microsoft.com/en-us/um/people/lamport/pubs/s...

Not only is TLA just as powerful as dependent types, it is far simpler[1]. Lamport says that the reason PLers aren't interested in TLA+ is because it's so simple, so there's not much to write about it. You see plenty of papers about embedding all kinds of things (separation logic, cost models, concurrency etc. etc.) with dependent types, things that are so trivial in TLA+ that they're barely worth a mention. Ideas from Hoare logic, behavioral refinement, differences between notions of program equivalence from process calculi (trace equivalence vs. bisimulation) simply collapse into simple, familiar logic in TLA (the only thing missing is probabilistic reasoning).

Lamport wrote about his experience trying to publish a paper showing that specifying real-time systems with TLA is trivial (it's a matter of defining a time variable): http://research.microsoft.com/en-us/um/people/lamport/pubs/p... You can only write a few papers on a simple approach that solves many problems, but lots and lots of papers that show how to use complicated approaches to solve them.

A lingua-franca must be simple. TLA+ uses notation and concepts that are familiar to all mathematicians and all computer scientists, plus a couple of new concepts that can be learned in a few days. Dependent types (and intuitionistic logic) are almost as arcane today as they were decades ago, virtually unknown outside the circles of logic and PLT, each of them is a particularly isolated sub-discipline within math and computer science. That so many papers are written about dependent types is strong evidence that they cannot serve as the lingua franca, and pretty conclusive proof that they cannot serve as the lingua franca just yet.

That PLers, as Lamport writes in his comment on my post, fail to see that Plotkin's SOS is an abstract state machine, and that some fail to see that computing a set-theory function and a type-theory function are two different computational problems with radically different computational complexity is further evidence that language models obscure rather than reveal.

Of course, as Lamport also says, real-world programming is very complicated, and so programming languages are justifiably complex (and whether dependent types can help with that remains to be seen[2]). But that complexity is absolutely not required for the purpose of a lingua franca with clear and simple semantics (TLA's semantics are far simpler than any programming language) for the purpose of specifying and analyzing algorithms.

Disclosure: I've contributed some code to the TLA+ project.

[1]: Not only do properties ("types") and algorithms share the same terms in TLA+, they are the same objects. This confuses some people to believe that TLA+ doesn't support higher-order algorithms, when, in fact, it becomes a non-issue. Instead of a parameter of a certain type, you have a concrete program that is the type (e.g., the program that nondeterministically returns, say, any even integer).

[2]: I'm skeptical because I believe we're close to the "Brooks limit": http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...


A couple of clear, encouraging, articles about how to use TLA and the benefits it provides would pay dividends (to both you and your readers) orders of magnitude greater than this obscure, roundabout, oblique approach.

> This confuses some people to believe that TLA+ doesn't support higher-order algorithms, when, in fact, it becomes a non-issue.

An article explaining this would be astonishingly interesting (and probably clarify this whole discussion).


That PLers, as Lamport writes in his comment on my post, fail to see that Plotkin's SOS is an abstract state machine

Is this even true? I don't think I've ever met a PLer who didn't know that an operational semantics describes an abstract machine.


I am curious what you think of math.andrej.com/2016/08/30/formal-proofs-are-not-just-deduction-steps/


He mostly talks about proof assistants for general mathematical theorems, something I don't use, but in TLA+, proofs are of logical formulas, the steps are logical formulas (unlike in dependently typed provers), and a computation is just a (temporal) logical formula, so TLA+ already lets you incorporate computations into proofs, but the process isn't automatic. Then again, TLA+ isn't really designed nor used as a general theorem prover (though it certainly can prove general mathematical theorems) but as a tool to specify and verify algorithms.




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

Search: