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 . 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 .)
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.
 powers of 10: https://www.youtube.com/watch?v=0fKBhvDjuy0
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.
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.
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.
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.
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 :-)
>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) 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.
 For example, with no oracles, we receive all of constructive mathematics, etc.
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.
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.
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?").
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.
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.
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.
> 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.
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.
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.
Um, well the computation (can be set up to) proceeed(s) on algebraic datatypes, so this seems trivially easy.
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!" ?
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.
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.
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.
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.
> 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!
Maybe this enumeration is the "external collaborator" in this case, but it's a very simple one.
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).
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.
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.
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.
(0) Computational complexity. Neither the lambda calculus nor Turing machines were invented to answer questions of computational complexity.
(1) Functions at types other than `nat -> nat`. Curiously enough, programming in the real world is seldom about evaluating functions of type `nat -> nat`.
Since computers regularly implement exactly such a mapping, it doesn't sound like a problem.
>Curiously enough, programming in the real world is seldom about evaluating functions of type `nat -> nat`.
How is it not about that? Everything you do is converted down to CPU ops that just implement (something expressible as) functions on natural numbers (technically, fixed-with binary numbers). The whole job of programming can be described as "converting a problem to a format suitable for a fast `nat->nat`-implementing machine"; it's just that several of the layers of the conversion are hidden from you.
That's the thing. In some languages, this mapping doesn't always exist.
> AIUI, the CTT is equivalent to saying that anything that can be computed at all (regardless of type signature) can be done via the `nat -> nat` functions representable on some TM.
The Church-Turing thesis says absolutely nothing about abstraction barriers your language might enforce, e.g., what you get if your language has parametric polymorphism (and no means to circumvent it, e.g., reflection).
These abstraction barriers might seem just like limitations that buy you nothing, but that's not the case. For example, if your language has abstract types (not the same thing as abstract classes), then you can be sure that any internal invariant violations can be traced to the module where the abstract type is defined. Have fun getting a static guarantee of this kind in C or Java.
> How is it not about that? Everything you do is converted down to CPU ops that just implement (something expressible as) functions on natural numbers (technically, fixed-with binary numbers).
Compilation translates programs in a source language into semantically equivalent programs in the target language. Compilation doesn't guarantee that every target language program is expressible in the source language - in fact, this is often not the case.
The mapping exists, just not necessarily within the language; the CTT is orthogonal to practical difficulties of massaging the data into a usable input format. (e.g. how to convert a binary tree in to the TM's format and vice versa)
>The Church-Turing thesis says absolutely nothing about abstraction barriers your language might enforce, e.g., what you get if your language has parametric polymorphism ...
Those all speak to the issue of how difficult it is (for e.g. a human) to implement the function, not whether language/computation model can compute it at all.
>Compilation translates programs in a source language into semantically equivalent programs in the target language. Compilation doesn't guarantee that every target language program is expressible in the source language - in fact, this is often not the case.
If you have a computation for which no TM (or asm, C, etc program) exists that computes it, let us know! That would be real progress on the CTT towards a negative answer and a Fields Medal for whoever found it!
In practice, people write their programs in a programming language. Some languages (e.g., C, Java, Lisp) only provide leaky abstractions, so programmers always have access to the internal representation of everything, to the detriment of modularity. But there are languages (e.g., Standard ML) that aren't hobbled in this way.
> Those all speak to the issue of how difficult it is (for e.g. a human) to implement the function, not whether language/computation model can compute it at all.
No. In Standard ML, writing a function that inspects the representation of an abstract type isn't “difficult” - it's literally impossible. If you want to do it, you have to use a different language. The type system enforces the separation of concerns, so that you don't have to rely on your discipline alone.
> If you have a computation for which no TM (or asm, C, etc program) exists that computes it, let us know!
Re-read my sentence. I was talking about the converse: There exist programming languages that don't allow you to do everything the target machine can do.
Alright, at that point it becomes an issue of "what kinds of things count as computations" for the purposes of the CTT. You're right that some languages simply lack certain capabilities, but that's an issue of access, not computation per se. You can get the same result in pure math:
"C is incapable of computing the zlobnorg of a matrix."
'Ridiculous! I'm sure I can write a program that does it! So, what exactly is a zlobnorg?'
"Sorry, only the matrix itself can answer that."
If you're going to go that route, then yeah the CTT is false -- likewise, TMs can't see inside black holes, so they can't "compute" that either.
But the "computations" referred to in the CTT are assumed to meet certain criteria, e.g. that there's some API exposed for accessing the relevant information, and the output is a "pure function" of that input (or at least makes any external state changes accessible, etc). But then once you've done so, all the Turing-complete languages can access said information information and compute the correct result.
Now, if your point is that the day-to-day work of a programmer is a lot more than writing pure functions: I whole-heartedly agree and have said the same thing myself. I cringe at the whole "Maxwell's equations of programming". Of course you have to care about external state and access privileges and race conditions and whether the API is usable, etc -- things that the CT notion of "computation" doesn't deal with. But, for the same reason, that's also orthogonal to the CTT.
Types determine what computations make sense.
> If you're going to go that route, then yeah the CTT is false -- likewise, TMs can't see inside black holes, so they can't "compute" that either.
Careful! I never said the CTT is false. I only said it guarantees nothing about functions whose type is anything other than `nat -> nat` (up to isomorphism).
> But the "computations" referred to in the CTT are assumed to meet certain criteria, e.g. that there's some API exposed for accessing the relevant information (...) Of course you have to care about external state and access privileges and race conditions and whether the API is usable, etc
These are properties of programs, not functions. Two syntactically different programs may compute the same function, so you can't conflate programs with functions (and hope to make sense).
Types determine what the developer has certified as making sense. There can (and as far as we know, always does) exist an isomorphism between the higher-typed function that the developer has implemented and the TM-computable nat->nat.
So, a TM can "make sense" of the higher-order function, even when it only has the nat->nat type.
>Careful! I never said the CTT is false. I only said it guarantees nothing about functions whose type is anything other than `nat -> nat` (up to isomorphism).
And and I was saying that the CTT is equivalent to saying that there is an isomorphism between a TM-computable nat->nat and any function that can be computed at all.
>These are properties of programs, not functions. Two syntactically different programs may compute the same function, so you can't conflate programs with functions (and hope to make sense).
Fair enough -- I should have said "function" there but the point stands: you can't refute by CTT by defining Turing-complete language that lacks some critical access and say, "well, that's a function I guess it can't compute!"
Types determine what computations make sense, even before any program is written at all.
> There can (and as far as we know, always does) exist an isomorphism between the higher-typed function that the developer has implemented and the TM-computable nat->nat.
Are you sure you're talking about isomorphisms in the mathematical sense? https://ncatlab.org/nlab/show/isomorphism I'm talking about a pair of morphisms:
forward :: Foo -> Bar
backward :: Bar -> Foo
backward . forward = id :: Foo -> Foo
forward . backward = id :: Bar -> Bar
> And and I was saying that the CTT is equivalent to saying that there is an isomorphism between a TM-computable nat->nat and any function that can be computed at all.
What category are you working on?
> you can't refute by CTT by defining Turing-complete language that lacks some critical access and say, "well, that's a function I guess it can't compute!"
I'm not refuting the Church-Turing thesis! Why would I want to? I even believe it's true... in some models. (Yes, truth is relative to models of a theory. Unlike provability.) I'm only saying that the CTT only claims what it claims. You're making extra conclusions that don't follow from the CTT's statement.
>Types determine what computations make sense, even before any program is written at all.
>What category are you working on?
I have no idea what point you're trying to make with either of these comments.
>I'm not refuting the Church-Turing thesis! Why would I want to? I even believe it's true... in some models. ...
Regardless, my point is that the limitations you're bringing up seem to be very trivial and understate the extent to which it does apply. You're still wrong if you think the CTT is "true, but false if applied to matrix functions. No way could a computer handle that. They only know binaries numbers, not the matrix type. I mean, come on, I gave them a different name and everything!"
The inhabitants of the type `forall a. a -> a` (which, by the way, in an effectful, Turing-complete language, has more inhabitants than just the identity function) aren't in one-to-one correspondence with the inhabitants of the type `nat -> nat`. I asked for an isomorphism of types, you have to give me an isomorphism of types. Or maybe you don't know what “isomorphism” means in mathematics?
>> What category are you working on?
> I have no idea what point you're trying to make
Okay, you don't know what “isomorphism” means in mathematics.
> You're still wrong if you think the CTT is "true, but false if applied to matrix functions.
The CTT isn't “false if applied to matrix functions”. The CTT says nothing about functions at a type not isomorphic to `nat -> nat`. It would be like saying “SilasX is all wrong about frogs!”, when you never said anything about frogs (at least, in this discussion).
> No way could a computer handle that. They only know binaries numbers, not the matrix type. I mean, come on, I gave them a different name and everything!"
I write my programs in high-level programming languages, not machine language, though. The whole point to high-level programming languages is to reason in terms of their abstractions, not their possible implementations.
For an analogy, you can map all the natural numbers to real numbers. This proves just about nothing. That you cannot map all the reals to the naturals proves something very important.
It would be truly bizarre if a useful programming language could express something that computation on bits could not.
If you can't map higher-order constructs to Gödel codes (effectively, numerical representations of syntax), you can't always map them to `nat -> nat`. That's precisely my point.
And, if you could map higher-order constructs to Gödel codes, the higher-order abstractions would be lost - all you need to do to break the abstraction is inspect the syntax. Just like, if you have reflection, type abstraction is lost - all you need to do to break the abstraction is use typecase.
As long as f(n) outputs a unique m, you can number f, n, and m. And as long as a programming language is Turing complete, you can do that. Interpreting any sort of abstraction is beside the point (even the "Gödel sentence" that you could ultimately find needn't be interpreted... which I suppose in this case would be a "Gödel operation").
Insofar as a program can be compiled and implemented in machine code, all the functions of that program's programming language can be mapped 1 to 1 to nat -> nat operations. This is just what's at issue here.
To cut through it a bit, you write
> The Church-Turing thesis says absolutely nothing about abstraction barriers your language might enforce, e.g., what you get if your language has parametric polymorphism
If a language has parametric polymorphism, is it therefore not Turing complete? Because if the language with parametric polymorphism is Turing complete, then the Church-Turing thesis absolutely has something to say about that language.
That mapping is a property of the implementation, not of the language. A user of the source language can't rely on the existence of this mapping - it would be literally impossible to run programs, say, using paper and pencil.
> If a language has parametric polymorphism, is it therefore not Turing complete?
> 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`.
No argument about it. But notice that this applies to programmers, not computers.
The article is about two groups talking past each other because of different terminology. When you say that "programming in the real world is seldom about functions of nat -> nat" you are doing the same, due to badly defined meanings of "programming" and "functions".
It applies to computers, because it's the computer itself that's preventing you from giving it certain classes of wrong instructions. I'm talking about enforcing things mechanically (type checking), not socially (design patterns, best practices, etc.).
If you consider that data to be a program, and the resulting messages to be errors, that is completely up to you.
As far as a typed high-level programming language is concerned, a syntax tree that doesn't type check isn't a program, so the question of what it does at runtime is simply ill-posed.
This is how Krishnaswami frames things. From the TOC perspective, there is no such thing as functions at all. Computations consume and produce strings. Both Church and Turing explain how those strings can encode the natural numbers (there was no talk of types by either). Interpreting a computation as one computing functions on the natural numbers or any other set is an entirely interpretive activity that is external to the computation itself.
I could choose a function between any two countable sets, e.g. (Nat -> Nat) -> (Nat -> Nat): pick a representation for the input and output and all models can compute the same functions, and those are the functions that machines can compute. They differ in abilities regarding representation within the model, but as the language models' representation require very significant computational work, I'd expect their representation to do more: they're paying for it.
A C compiler works hard, so you'd expect it to provide you with a representation more suitable to your wishes than machine code. It's just that as a compiler like C translates a "meaningful" language to a machine encoding, everybody notices the work. The language "computation" models work in a vacuum, so I just pointed out that even though they don't translate anything from one representation to another, they still have to pay for their natural representation.
There isn't a TM-suitable representation for things of type (Nat -> Nat). No matter how you try to encode a Nat->Nat as a Nat (or a bitstring, if you prefer), you're going to screw up equality (which means you're actually encoding some other type). You'll map two unequal functions to the same Nat, or (more likely) map one function to multiple unequal Nats. This is the difference between how lambda calculi and Turing machines handle higher-order things: A Turing machine can always inspect the "internals," so you need an actual bijection from functions to strings, whereas lambda calculus hides the internals, so it's safe to map one function to multiple syntactic representations.
This shows that the concept of a type requires actual computational work rather than just a matter of “free” perspective. Your mere presentation of a function as an inhabitant of a type creates a computationally harder problem than presenting a function as a mapping between sets. Put differently, when a typed language model computes a function (Nat -> Nat) -> Nat, it does more work, and solves a harder problem than necessary to compute that function in the normal set-theory sense. You can choose to solve that problem on a TM by simulating type checking if you like, but you can’t compare “compute a function in the set-theory sense” and “compute a function in the type theory sense”, because those are two different problems with two radically different computational complexity costs. You can decide to do that extra work or not (you may want to because you gain benefit from it), but you can’t compare a model that always does — and pays handsomely for it — with one that doesn’t.
Otherwise, I could create a language model that solves all NP problems in polynomial time by defining my language as requiring a proof certificate with every input problem, which my model would then check in polynomial time. No one would believe my language actually really solves a computational problem: it simply pushes the difficulty to the collaborator.
Equality is also an internal question. Define any relation between two sets (your definition of equality), and all models would be equally able (or unable) to decide it.
People who use set theory as their foundations impose on themselves the even harder task of making sure their mappings are coherent w.r.t. whatever notion of structure they want to work with, i.e., homomorphisms in a category of interest.
> Otherwise, I could create a language model that solves all NP problems in polynomial time by defining my language as requiring a proof certificate with every input problem
No, this is wrong. Changing the input type means that you are not, in fact, solving the original problem.
Let's not get into this old debate because we'll never get out of it. Suffice it to say that it that there is no doubt that Turing and Church (and Gödel and von Neumann) used set theory as their foundation, and when they said "function" they meant a set-theoretic function, namely a mapping from a domain (set) to a range/co-domain (set). If by "function" you mean a type-theoretic function then you're talking about a computationally harder problem, as you need to compute the underlying set-theoretic function and check a proof. You can certainly ask a TM to simulate a type checker and compute a type-theoretic function. There's actual work involved, and someone must do it. You cannot say that your formalism gives it to you for free, or you'll have a formalism that proves things for free, which is impossible.
> Changing the input type means that you are not, in fact, solving the original problem.
Exactly! But that is precisely what you do when you interpret "function" to mean a "type-theoretic function", and solve a different problem. Any work that needs to be done under the normal meaning of "function" also needs to be done in the typed formalism. If you need to ensure/prove something, there is work and computational complexity involved. Pushing it to a collaborator doesn't make it disappear (let's call this the law of preservation of computational complexity). Someone has to do it, and in no model does it suddenly become free. It's perfectly OK to say that you start counting after much of the hard work is done, but in that case you need to say that your model requires upfront work, and therefore cannot be compared to models that don't. That's my whole point.
BTW, any logical formalism forces you to pay attention to meaning; choosing to encode the logic in types has advantages and disadvantages, but it is not at all the only way to logically describe a program.
Pray tell, what's the use of a computation without paying attention to its meaning? My use case is simply “knowing the meaning as early as possible”, and there ought to be no discussion that this should be everyone else's use case as well. Nobody performs a computation without some sort of expectation about the relation between the inputs and the outputs.
> BTW, any logical formalism forces you to pay attention to meaning
I never said types are the only way. For instance, you could use Hoare logic, but it's notoriously more difficult to use, precisely because it gives programs no a priori meaning.
First, I don't think that the only way to assign meaning to computation is by formally assigning meaning to the syntactic components that comprise its program, as written in some human-readable language. Most of the relevant meaning is in human interpretation of the input and output or the sensors and actuators. Components' meaning may be stated informally. I am not aware that formal meaning is the only valid meaning. People wrote the software that landed men on the moon in assembly; that was pretty meaningful. I believe this is still the prevailing view in computer science.
Second, you keep identifying the notion of computation with the notion of a program written by a person. The theory of computation, from its earliest days -- by Turing himself -- has studied computational phenomena in neural networks, genetics (Turing was a pioneer of both NNs and genetic algorithms) and quantum phenomena. Some of the greatest achievements in CS are not specifically related to software (I count at least 20% of all Turing awards).
> For instance, you could use Hoare logic, but it's notoriously more difficult to use, precisely because it gives programs no a priori meaning.
Or TLA+, which makes types notoriously more difficult to use by comparison.
Please suggest alternatives - that actually work.
> Most of the relevant meaning is in human interpretation of the input and output or the sensors and actuators.
The relation between the input and the output. This can only be stated formally.
> Components' meaning may be stated informally.
That leads to disaster very quickly.
> I am not aware that formal meaning is the only valid meaning.
Well, I am. Too much nonsense has been said as a result of not formalizing things.
> Second, you keep identifying the notion of computation with the notion of a program written by a person.
No. Even if a computation “arises in nature” (which is just your way of looking at things, actual physical phenomena is what you can measure, plain and simple), the only way to make sense of it is to write a program that reproduces the computation. This is how scientific theories work.
> Or TLA+, which makes types notoriously more difficult to use by comparison.
Some type systems are more difficult to use than others, and the type theory community is definitely guilty of not paying enough attention to usability, but I don't see how model checking has a higher power/cost ratio than sensibly designed type systems. Which tool satisfies the following criteria?
(0) Compositionality: you can understand a large system by studying its parts in isolation.
(1) Handles higher-order constructs (first-class functions, objects) gracefully.
(2) Stops you from saying nonsense as early as possible.
I rest my case.
AFAIK, the only languages that fully express the computational meaning formally with types are the dependently typed ones. AFAIK, there has been exactly one non-trivial real-world program written in such a language, and its author wasn't too pleased with the process (I'm referring to CompCert and Xavier Leroy). Every other program in every other languages has most of its meaning expressed informally, in the mind of the programmer. Unless you believe that no programs work, then nearly all programs that do express most of their meaning informally.
> Too much nonsense has been said as a result of not formalizing things.
Formalizing things doesn't imbue them with good sense. You can state plenty of nonsense formally. The only thing you're guaranteed is that it's consistent nonsense, and, as someone said on one of my favorite TV shows, "The sole virtue of the ineffectual is consistency".
> Which tool satisfies the following criteria? ...
TLA+, and far more elegantly and simply than any typed language you've seen.
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.
> 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).
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, and this.
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, and this.
I read them ages ago when you first suggested them to me. The impression of TLA+ I got was far from compelling in the composability stakes. I suppose I could go Googling for info on how TLA+ is composable but if you know the answer yourself why not explain it or point me to a specific article which explains it?
Thing is, TLA+ does what specification languages are supposed to do. It is just an exceptionally small and elegant specification language. It may feel like groundbreaking to people who have never used specification languages. Haskell is not a specification language. It's a programming language, therefore it is much more complicated -- like all programming languages -- and much weaker -- like all programming languages. There are programming languages that seek to do what both specification languages and programming languages do. Examples include SPARK, Coq, Agda. Of them, the only successfully used language is SPARK, but it is limited as a programming language. Coq and Agda have never been used for large programs, so nobody knows if they work at all. Early results (like CompCert) are not promising. TLA+ is used on very large projects every day at Amazon, Oracle and Microsoft. No academics are involved. Same goes for other specification languages like Z.
Because for years the PL community has been trying -- without success -- to combine a specification and a programming language into one, someone who's familiar with programming languages may view specification languages as groundbreaking, but they've been doing their job for decades. They just don't try to do what the PL community is trying which is to also serve as programming languages. Once you give that up, the things you want and that are so hard to get become much easier.
Here's how things become easier:
1. There's a result (mentioned in my Curry On talk/post) that simply put states that correctness doesn't compose. In intuitive terms, if your program consists of 10,000 functions, each 3 lines long, composed in various ways, you can't prove global properties by doing simple proofs that are as easy as you'd expect for 3-line functions, and have the global result pop out. The idea of the proof is very simple: in computations, complexity builds up very fast. A TM with 6 control states can have 10^35,000 states or so, and states in sub components simply cannot be hidden. The way to tackle that is not to try to prove the global properties directly from the local properties, but to describe the entire program in various abstraction levels and then prove that each lower level refines the higher one. This is very hard to do in programming languages at scale. In a specification language, you have better control over level of abstractions and what details you want to leave out.
2. There's nothing external; I.e. there's no IO. An example of something that's very important to prove is, e.g., if you read a certain record from the DB many times, its "last_updated" field gorws monotonically. I don't know how you can try to do it in a programming language. In a specification language, you specify the entire system -- the DB, the network, the OS, the users -- and you do it in the abstraction level that precisely suits your needs. There is no information overload and no missing information. You write your assumptions, and hope to get verification for your claims.
3. There's no need for efficiency. You can freely use simple mathematical definitions whose "automatic" implementation is extremely inefficient, because the code never gets executed.
So, specification languages work, and have worked for a long time. What doesn't work is a specification language that's also a programming language. That would be truly groundbreaking, but I don't think anyone is even remotely close, or is even looking in the right direction.
> I suppose I could go Googling for info on how TLA+ is composable but if you know the answer yourself why not explain it or point me to a specific article which explains it?
See chapter 10 of this freely downloadable book http://research.microsoft.com/en-us/um/people/lamport/tla/bo...
The problem here may still be that you're thinking of composability in terms of functional languages instead of composability of abstract programs. The book does not translate the terms you're familiar with to TLA+ terms because it doesn't assume any existing predilections. For example, you're used to thinking of the "map" function as a higher-order algorithm. That doesn't mean that's what it is; that's just how it's described in Haskell. Another way of looking at it is that map is nondeterministic. The book won't tell you that what you know as parameterization is just another form of many of nondeterminism (concurrency, IO are other forms). If you have nondeterminism as a built-in construct, there's no need to work hard on higher-order things; they're just special cases. But, again, the book starts "from scratch" and doesn't assume that you're used to thinking in Haskell. So there's no lack of material; there just isn't a dictionary for people who are already used to thinking about things in some specific way. I hope to write such a dictionary one day.
Absolutely, and thus types and specification via TLA+ are not in opposition. In fact they can work in harmony.
> someone who's familiar with programming languages may view specification languages as groundbreaking
That's not what I find groundbreaking. What I find groundbreaking is that TLA+ is (supposedly) so composable despite being so simple. I remain skeptical. Indeed, even the fundamental TLA+ notion of "priming" variables seems that it would immediately be an impediment to composability.
> There's a result (mentioned in my Curry On talk/post) that simply put states that correctness doesn't compose.
Yes, I recall that. I believe the theoretical result, of course, but I am yet to be convinced of its practical relevence. Correctness does compose in my experience as a mathematician and as a software developer. In fact, I can't see any way that correctness can be achieved except through compositionality.
> A TM with 6 control states can have 10^35,000 states or so
Please explain your terminology. Surely it can have infinitely many states? Indeed a Turing machine with 1 control state can have infinitely many states.
> states in sub components simply cannot be hidden
I find this a very puzzling statement. States in subcomponents can be easily hidden in every common-or-garden programming language.
> You write your assumptions, and hope to get verification for your claims.
Sure, but as we've observed, it doesn't actually tell you anything about the final implementation you come to write.
> The problem here may still be that you're thinking of composability in terms of functional languages instead of composability of abstract programs.
I'm thinking of composability in terms of building things out of smaller things and being able to deduce properties of the things based on the properties of the smaller things. That notion precisely captures "composability" (even "compositionality", if we want to get formal) as far as I am concerned. What does it mean to you?
> The book won't tell you that what you know as parameterization is just another form of many of nondeterminism
OK, but you could. What exactly does that mean?
Sure, it's just that TLA+ can open your mind to the idea that you may not need types for things you think you do -- even in a programming language. It can also show you how you can do mutation and still remain pure without using monads or any higher-order function composition. This idea is used in synchronous programming languages, too, so this is something that definitely applies to programming languages.
> Indeed, even the fundamental TLA+ notion of "priming" variables seems that it would immediately be an impediment to composability.
Why? It's a perfectly pure operator and it distributes. Op(x, y)' = Op(x', y'), assuming Op doesn't have any other variables in it, i.e., it's a "level 0" operator.
> Correctness does compose in my experience as a mathematician
I can show you a trivial example of why that's not true: the gravity equation. Everything composes, yet two instances are already chaotic. You can't extrapolate almost anything you know about the gravity equation to predict the bodies' positions over two instances. For discrete processes, such chaotic behavior is small potatoes. We don't even use the word "chaotic" because we're way beyond that. The problem is this: if everything is simple, you can compose correctness. But when everything is simple, composition isn't really required. This is what I'd like to call the "FP extrapolation problem". FP works beautifully for simple examples, i.e., where new approaches don't really matter. People then extrapolate from toy examples and assume it can scale (in spite of the theory that says otherwise), yet no one has yet shown that it does in practice. By that I don't mean that you can't write large programs in FP. Of course you can. But the advantages that are very clear in the simple cases (where they don't matter), start dissipating and you just don't see a drastic effect at scale (maybe the effect is even negative; nobody knows).
> Please explain your terminology.
Sorry, I meant a TM that terminates eventually. I think that's either the current record or the lower bound. Don't remember.
> I find this a very puzzling statement. States in subcomponents can be easily hidden in every common-or-garden programming language.
They're hidden from the programmer's view, not from their effect on correctness. That is precisely the result that says that verification isn't fixed-parameter tractable. Namely, if the cost of verification is O(|S|) when S is your number of states, you can't say, well, each of my components has n states and I verified them individually, and now I want to compose k components, and so the cost of verification would be O(small function of k). It will be O(n^k) or something like that.
> Sure, but as we've observed, it doesn't actually tell you anything about the final implementation you come to write.
Right, but nothing else can, either, unless you do end-to-end verification, which is far beyond what 99.9% of projects can afford to do (or need to). Here is where you rely on software engineering practices, tests and whatever tools you have for local properties that help prevent easy bugs (like types and static analysis). There is nothing that can help you prove interesting logical properties at this level, at anything close to an acceptable cost.
> What does it mean to you?
Oh, the same. It just doesn't look the same way in TLA+, where you compose things as A ∧ B rather than A(B) (they don't mean the same thing).
> What exactly does that mean?
Alright, let me try: suppose you have a higher-order function, say `filter`, that takes a function of type `a -> bool` (where a is a type parameter), and filters a list. Now suppose you want to prove that, say, the length of the resulting list is no bigger than the input list. In a functional language you say, I have a function parameter `p` that could be anything of the appropriate type `a -> bool`. In TLA+ you don't need this because you can say that p is not a parameter of a certain type, but a concrete, specific program that nondeterministically returns either TRUE or FALSE. You prove your theorem for that specific p, but it really covers the same as all predicates p of that type.
The cool thing, then, is this: you can ask, what is the relationship between that nondeterministic program p, and a deterministic program p1, that, say, returns true iff its argument is an even number? Well, it's a refinement relation (any behavior of p1 is a behavior of p, but not vice-versa), and in TLA+ this is expressed simply as p1 => p, where => isn't some special notation but the same-old familiar implication operator from propositional calculus, because in TLA+, a program is a binary boolean predicate that evaluates to TRUE iff there's a next-state relation between its two input states, the unprimed and primed.
The key to that is understanding the model (in the logical sense) of a TLA formula (i.e. a program). The model is a set of all possible behaviors, where a behavior is a sequence of states (similar, but not exactly a trace in the process-calculi sense). So a program is a set of behaviors. A program property (i.e., the program never sends the character "x" over the network), or a "type", is the set of programs that satisfy it (I mean by the simple isomorphism between predicates and sets). Here is the crucial bit: as the TLA logic only allows to specify properties that must be true for all behaviors or none (hence the problem with probabilistic algorithms), there is no need to keep the behavior sets for each program in the "set of programs" separated, and instead of a set of programs -- i.e. a set of sets of behaviors -- a program property can simply be a set of behaviors. But a set of behaviors is a program! Therefore a program property, or a "type", in TLA is the same thing as a program. Program properties and actual algorithm specifications become a hierarchy of nondeterministic programs that refine or abstract one another. So the program that does parallel merge-sort is a refinement of a program that does some sort of merge sort, and that, in turn is a refinement of a program that "sorts somehow". And all those relationships are simple propositional calculus connectives, and you can reason about what kind of low-level steps a low-level specification does for each abstract step in a higher level specification.
I'm very much hoping this will be the case!
> > Indeed, even the fundamental TLA+ notion of "priming" variables seems that it would immediately be an impediment to composability.
> Why? It's a perfectly pure operator and it distributes. Op(x, y)' = Op(x', y')
> 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.
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.
That's the same sense in which Neel means it.
See also https://news.ycombinator.com/item?id=12403508
I agree with you on this one. What actually exists in computing is procedures, which may or may not compute functions. For instance, even in Haskell, so-called “functions” may call `error` or diverge.
However, it's very useful to treat extensionally equal procedures (considering both their effects and their final results) as equal, even if they're syntactically different. This is the basis for compiler optimizations. And the lambda calculus (suitably extended with effectful computations) is better equipped than any machine model to make this identification.
(OTOH, the lambda calculus is a grossly inadequate foundation for concurrency, which is about communication, rather than computation. The main solution I've seen proposed by proponents of functional languages, namely, abusing callCC to get something like cooperative concurrency, is very, very, very bad.)
> Interpreting a computation as one computing functions on the natural numbers or any other set is an entirely interpretive activity that is external to the computation itself.
In practice, people care about the meaning they ascribe to the symbols with which they compute. We use symbols to denote. A meaningless symbol might as well never have been computed at all.
You can't free yourself from thinking in terms of languages :) Not a single one of the machine models -- TM, RAM, neural networks, DNA, digital circuits, quantum computers -- has a concept of a procedure. Procedures are language constructs. Whether you choose to compile Pascal or Haskell to x86 machine code is up to you, but in either case there would be a complexity price to pay.
Machine models take bits and they compute bits, period. Like an apple that falls, they just do they're thing. If a person then wants to say, hmm, that apple's path describes an integral of acceleration, or I will assign the input and output bits mathematical objects, and say that the mapping is a function -- they're welcome to do it, but it's not what the computation does.
> A meaningless symbol might as well never have been computed at all.
Everyone agrees on that. But an apple that falls without Newton to grasp its meaning still falls, and a machine still computes. For meaning you have to pay real, measurable complexity. It therefore doesn't make any sense to compare a model that pays that price with one that doesn't.
Now would I want to. Why would I deprive myself of the benefits of compositionality, separation of concerns, or simply modeling the problem domain as faithfully as possible?
> For meaning you have to pay real, measurable complexity.
Complexity in the sense of complexity theory? I don't see how. If you mean the computational cost of type checking, that's in practice a non-problem as long as the type system is reasonable. (By which I mean: Types are first-order and there is no type-level computation beyond synonym expansion, so plain first-order unification can reconstruct out all the types. Damas-Milner is a special case of this.)
Or are you talking about complexity in some other sense? I don't see the requirement of making sense as a burden. I'd feel burdened if I had to deal with some random computation I found in the wild, with no indication regarding what its meaning is.
But now you're saying that you are interested in programming. TOC is about something else.
> Complexity in the sense of complexity theory?
> that's in practice a non-problem as long as the type system is reasonable.
Whether that's an issue for the questions you're interested in asking doesn't define what "in practice" means. It certainly matters for the questions TOC is asking. A model that requires a computationally powerful collaborator -- a programmer -- can't arise spontaneously in nature, for example.
> I don't see the requirement of making sense as a burden.
Again, burden is a question of meaning (proof: you need an agent for something to be a burden for). The requirement, however, shows that the different models are objectively, essentially and radically different.
If you're trying to argue that “computation” is a physical phenomenon in the same sense gravity or electromagnetism are, I have bad news for you: it isn't. The theory of computation, just like information theory and probability theory, is first and foremost a mathematical theory: It is a priori only constrained by the requirement to be logically consistent. This is very different to what happens with a theory of gravitation or electromagnetism, which has to match external observations.
> > Complexity in the sense of complexity theory?
> Whether that's an issue for the questions you're interested in asking doesn't define what "in practice" means.
In practice, when I submit a Standard ML program to a REPL, the REPL tells me almost instantly whether my program is typable or not.
> Again, burden is a question of meaning (proof: you need an agent for something to be a burden for). The requirement, however, shows that the different models are objectively, essentially and radically different.
Agreed. Only one of the theories is actually useful. (Urgh, it's not a model in the logician's sense!)
Don't know what you mean by "in the same sense", but Turing, von Neumann, Gödel and Hartmanis would have been saddened by your news because they thought (I guess Hartmanis still does) differently. So did Church. The very idea of algorithms -- as Church writes in his review of Turing's paper -- contains a notion of physical realizability. The idea of un/decidability -- only intuitively touched upon in Church's paper, and pretty thoroughly discussed in Turing's -- is predicated on the notion that a computational step takes at least some constant amount of physical time. It is true that a computation isn't a specific physical phenomenon like gravity, but a general, abstract phenomenon, that can be realized in different ways. But if it can't be realized, then it isn't considered computation, unless the people discussing it exclaim very clearly that they're discussing hypothetical computation.
Some people take it further and say that not only computation is physical, but as it is meant to model the work of the mathematician, it grounds all of math in the physical along with it, and things that can't be feasibly computed (in some reasonable amount of time) should be left outside the realm of math. You may have heard this story by Harvey Friedman about the ultrafinitist Alexander Esenin-Volpin who attended his lecture, and Paul Cockshott from the Univeristy of Glasgow writes this:
> 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.
I don't see how. That inherent complexity is precisely that computed by the machine (provided that you're talking about a function in the ordinary, set theory sense, rather than in the type theory sense, in which case a function is a set-theoretic functions plus a proof of set membership).
> and of course, you also turn around and favor certain interpretations over others based on the cost of embedding them in your favorite computation model
No, the complexity of evaluation differs in the different models by a small factor (polynomial at most), that is much smaller than the complexity differences of the representation. There is no room for (significant) interpretation here: the typed formalisms can perform computations of possibly arbitrary complexity during their validation stage. They aim prove something and proving something comes at a cost. There is no interpretation by which proving a possibly complex theorem is considered of having little complexity.
The same function may be computed by different procedures with different complexity.
> rather than in the type theory sense, in which case a function is a set-theoretic functions plus a proof of set membership
Not all types denote sets.
> There is no room for (significant) interpretation here: the typed formalisms can perform computations of possibly arbitrary complexity during their validation stage.
This is the price of capturing the meaning of computation. Of course it doesn't come for free. But, in general, the earlier you do it, the less work it requires. In the limit, if you do it really late (e.g., test suites), it requires an infinite amount of work (searching infinite input spaces).
The whole idea of computational complexity theory, the time- and space-hierarchy theorems, that are generalizations of the halting theorems and are probably the most important theorems in computer science, is that every function has an inherent complexity, that is independent of the algorithm that implements it. The time or space complexity of an algorithm may be greater than or equal to the complexity of the function. You may want to read my blog post about computational complexity in the context of software correctness: http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...
> Not all types denote sets
In this case, what matters is what set they specify (not necessarily denote) and what proof.
> This is the price of capturing the meaning of computation. Of course it doesn't come for free. But, in general, the earlier you do it, the less work it requires. In the limit, if you do it really late (e.g., test suites), it requires an infinite amount of work (searching infinite input spaces).
First, the computational complexity of verifying a program is the same no matter when it's done. Read my other blog post. Second, I'm talking theoretical computer science here. Obviously there are all sorts of interesting trade offs in real world programming. Finally, the whole point of this article is that language models do this extra computational work and solve a different problem, while the people discussing them often don't notice or point this out.
How does this even make sense? The whole point to specifying something abstractly is that you want to denote anything that satisfies the specification. And what proof are you talking about? Are you confusing “proof” with “typing derivation”? A single term may admit multiple typing derivations.
> First, the computational complexity of verifying a program is the same no matter when it's done.
You're assuming that you can write correct programs, without taking verification into consideration right from the beginning. This assumption is incorrect.
I am not confusing anything. Again, this is a matter of overloaded terms. When a typed language expression to compute a function Nat -> EvenNat is given, there are two computations that must be carried out: First, a proof that the function yields an even natural is computed (you call that type checking); second (that's the evaluation step), the actual computation is carried out, and an element in the set of even numbers is computed.
When you want to start counting operation is up to you. You can declare that the validation (type checking) phase is not counted. But the fact remains that if you know something -- i.e. that the result of the computation is a member of a certain set -- that knowledge must be gained at some computational cost. If you know it, then it means that something has paid that cost.
> You're assuming that you can write correct programs, without taking verification into consideration right from the beginning. This assumption is incorrect.
I am not assuming anything. When to do something is a practical, engineering concern. It is obviously of extreme importance. But from a theoretical point of view, the total computational effort required to prove a property of a program is the same (given the same conditions), no matter when it is carried out. Of course, engineering concerns move that complexity around between different machines -- the computer and the human programmer -- based on their respective strengths, but the total work is always the same. Just as to sort an array there's a minimum complexity required (O(n log n)) no matter how you do it, so too does writing and proving a program correct has an inherent complexity that has to be paid no matter what.
As stated above, not all types denote sets. For instance, in a language with general recursion, (simple) types denote domains, not sets.
> But from a theoretical point of view, the total computational effort required to prove a property of a program is the same (given the same conditions), no matter when it is carried out.
You are ignoring two things:
(0) There is no magical way to implement the correct program if you don't have verification in mind right from the start. You will implement the wrong program, then attempt to fix it, then have another wrong program, then attempt to fix it, etc. That too has a computational cost.
(1) When you design your program upfront with verification in mind, you actually have a different mathematical object than when you don't. (Just like 2 as a member of the naturals is a completely different mathematical object from 2 as a member of the reals.) If your program design is split into modules (as it should be, if your program is large enough), then enforcing abstraction barriers across module boundaries constrains the size of the design space, often dramatically. (e.g., there are too many non-parametric total functions of type `forall a. a -> a` to even form a set, but there is only one parametric such total function: the identity function.) You note that verified properties could be thrown away after the verification is done, but why would anyone in their right mind want to?
No, I'm not. I'm talking about math. (If you read my comment history, my distaste for “engineering” should be obvious, at least if by “engineering” we mean “software engineering”.)
> but theoretically a building would be just as strong if it were somehow built from the top down.
The amount of mental gymnastics required to produce this statement (not to mention expect someone else to believe it) completely baffles me.
> Computational processes in a living cell, for example, also have to ensure correctness -- and therefore spend computational resources on "verification" -- yet they don't use symbolic logic for that task.
Nature doesn't do “verification”, because there's no specification in the first place. Nature just evolves a variety of systems, and those that aren't fit enough to survive, well, just die. Also, the evolution of biological systems happens way too slowly to use it as inspiration for how to design computational systems for our own purposes.
Good. In that case, verifying that a program conforms to spec in the general case is of as much computational complexity no matter when it's carried out. This is proven and well known. For an overview, you can see my post here: http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...
In short, the reason for that is that the every computational problem with a computable upper bound on complexity can be efficiently reduced to verification. The complexity required to verify is a function of the spec, and can be made arbitrarily hard.
> The amount of mental gymnastics required to produce this statement (not to mention expect someone else to believe it) completely baffles me.
OK, so let me use another analogy. That you can wind up a wind-up toy before I enter the room doesn't mean that just because you hid that from me, the toy requires any less external energy to run than when you'd wind it at any other time. Discussions of ergonomic ways to wind the toy (with a larger lever perhaps) may be interesting, but they're separate from this basic fact.
Verification is a computational problem, and one of a certain complexity. That complexity must be paid, no matter what, no matter when. The knowledge that a certain program has a certain property has a price-tag, and there are no discounts. Because all computational problems efficiently reduce to verification, if you believe you've found a loophole, I could use it to solve much bigger problems than ensuring that your recipe application is correct.
> Nature doesn't do “verification”, because there's no specification in the first place. Nature just evolves a variety of systems, and those that aren't fit enough to survive, well, just die.
You're wrong because, again, you're blind to computational complexity and to computational processes that aren't man-made programs. What you described is precisely how nature computes. That things that aren't fit enough to survive "just die" is a verification process by a genetic algorithm (that requires tremendous time and space complexity) to conform with the spec for genes -- i.e. life's "software" -- which is: reproduce.
Computational complexity results are used in the study of biological systems. Look at the work by Leslie Valiant (Turing award) or Stuart Kauffman (https://en.wikipedia.org/wiki/Stuart_Kauffman). Incidentally, TLA+ can also be used to model systems such as metabolic pathways, as those are very easily described as nondeterministic state machines: http://www.cosbi.eu/research/publications?pdf=5437
> Also, the evolution of biological systems happens way too slowly to use it as inspiration for how to design computational systems for our own purposes.
Maybe, but TOC doesn't study how to design computational systems for our own purposes. It's pure science. If its discoveries turn out to be useful, then that's a happy coincidence.
For that matter, neither does most of TOP for the past couple of decades or so. If you do math to study a system designed for use by a computationally-complex collaborator (the programmer in this case), you must study the collaborator as well. TOP shows no interest in such empirical study, and has therefore been utterly unable to prove that the approaches it advocates actually help write very large complex software systems; indeed it has been even unwilling to test this hypothesis, not even once.
Then, as Dijkstra said, don't focus on the general case: “So, instead of trying to devise methods for establishing the correctness of arbitrary, given programs, we are now looking for the subclass of "intellectually manageable programs", which can be understood and for which we can justify without excessive amounts of reasoning our belief in their proper operation under all circumstances.” https://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/E...
> The knowledge that a certain program has a certain property has a price-tag, and there are no discounts.
So what? If you're designing programs out of reusable components and you don't throw away their proofs of correctness, then much of the cost has already been paid by someone else before you even start.
> You're wrong because, again, you're blind to computational complexity and to computational processes that aren't man-made programs. What you described is precisely how nature computes. That things that aren't fit enough to survive "just die" is a verification process by a genetic algorithm (that requires tremendous time and space complexity) to conform with the spec for genes -- i.e. life's "software" -- which is: reproduce.
This still doesn't make sense. No biological system is “correct” in any meaningful sense. Correctness is always relative to a specification, and, even if your specification is as vague as “survive”, what's happening in nature is that some life forms are lucky enough to be fit for their current circumstances, not all possible ones.
Exactly, except that since Dijkstra gave that talk (early seventies) we have learned some important results in computational complexity. The bottom line is that we know that it is impossible to create a generally useful programming language (even not Turing-complete; even a finite-state machine) where every program is relatively cheap to verify (in 2000 it was proven that language abstractions can't significantly reduce verification cost even though it would have been reasonable to believe that they could; that result is discussed in my linked post). Whatever language is chosen, only a small subset of programs written in that language will be verifiable. Identifying that subset requires extensive empirical research. This is done in the software verification community; unfortunately the PL community is reluctant to conduct empirical research.
> much of the cost has already been paid by someone else before you even start.
Not true. See the Schnoebelen results quoted in my post that I linked to. Composing proofs of program correctness requires proof effort that is intractable in the complexity of each component, not in the number of components. This was proven in 2005. In technical terms, verification isn't Fixed-Parameter Tractable, or FPT, a relatively modern complexity class created to incorporate problems that are intractable in the general case but may be tractable in practice. In simple terms, that each of your components has been proven correct still means that the difficulty of proving the composite's correctness is an intractable function (exponential at least) in the complexity of each component. Of course, theoretically it's better than nothing, but not by enough.
> is that some life forms are lucky enough to be fit for their current circumstances, not all possible ones.
That is only if you view each life form as the computational system. However, that genetic algorithm I was referring to is conducted by all living systems as a single computational system.
You're still focusing on arbitrary programs. Just don't write arbitrary programs. Let your intended proof tell you what program you need to write.
> Composing proofs of program correctness requires proof effort that is intractable in the complexity of each component, not in the number of components.
So keep each component small.
> However, that genetic algorithm I was referring to is conducted by all living systems as a single computational system.
This is still not verification. It's just testing on a much larger scale.
Verification is hard. We all agree. But that is for the worst case. Alternatively we can say that it is hard to verify arbitrary programs. I am utterly unconvinced that it is hard to verify programs that are designed to be verified, and I am utterly unconvinced that it is hard to design programs to be verified.
How should I convince myself that it is hard either (1) to verify even programs that are specifically designed to be verified, or (2) to write such programs?
(I don't mean hard in practice, I mean in theory.)
Didn't we discuss that issue on Reddit? Anyway, as the complexity of verification is proportional to the number of states. If you write the program from scratch, the number of states is dictated by your spec (as every computational problem, every function has an inherent computational complexity). Your spec can be arbitrarily hard.
Now, it's not a matter of worst-case. That writing and verifying arbitrary programs is the very same problem is easy to see: given a program A, and a property I wish to verify P, I then create a spec S = A ∧ P, i.e, the program you write must behave like this arbitrary program and satisfy P. So there is no difference between writing from scratch or verifying. Indeed, you can see that static analysis tools can often prove on arbitrary programs the very same properties that are enforced by type systems.
Of course, not every algorithm and property are worst-case, regardless of whether the program is being written or given. There are useful classes of programs/properties that are easier to verify, and the language can make useful restrictions. So far, examples that work well in practice are SPARK and SCADE. Each forbids memory allocation, including unrestricted stack growth.
I don't follow. What has A got to do with it? I am given a spec P. You claim that it's hard to write a program that satisfies P, pretty much regardless of what P is. I don't see how A is relevant at all.
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.
Really? What's so special about strings? Perhaps I want computations to consume and produce trees. It seems like you've picked an arbitrary setting for computation and said "Look! My constructions which are naturally suited to this setting are naturally suited to this setting!".
So there's a real difference between various configurations of gas molecules in a box, and a real difference in the computational cost of representing them. Your statement is not unlike saying, "oh, so you've picked a high-entropy configuration, how convenient! What's so special about high entropy?" High entropy and low entropy aren't symmetrical. It takes more energy to move in one direction than the other.
Again, you shouldn't be surprised by this at all (I'd think it's rather obvious). Since typed formulations do proof work in their validation step (that can be Turing-complete in some cases), obviously that means that there is more complexity in their representation, otherwise, you'd have computation for free.
You can choose whatever representations you like. But representations that express more information, come at a higher computational cost.
I'm not sure why you think that I'm surprised, or even why you think that I disagree with your overall argument. I'm just trying to help you build your argument by pointing out the most obvious aspects which need more careful elucidation.
So your claim is that in the physical world strings are more fundamental than trees. Good to know. In fact I think there's an even simpler reason than the one you give of "entropy". That is, trees require space which grows exponentially in their depth, and thus they can't even be represented in the physical world.
A string is quite different from a stream. A string is typically considered random access, for a start.
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...
On Scott's blog Neel talked about functions '(unit -> bool) -> (unit -> bool) -> bool', but this example seems spurious. He asserted that Turing Machines could receive the arguments Godel encoded but the Lambda Calculus couldn't. I don't see why. If you also let the Lambda Calculus receive its arguments Godel encoded then it can inspect them and perform the same dovetailing that the Turing Machine would.
Do you know of a more compelling example?
I never said the Church-Turing thesis fails. I only said that it only claims what it claims.
> He asserted that Turing Machines could receive the arguments Gödel encoded but the Lambda Calculus couldn't. I don't see why.
In the lambda calculus, if you have the Gödel number of a Turing machine, you can simulate that Turing machine. But if you have a lambda abstraction, you can't produce the Gödel number of a Turing machine that computes the same (partial) function as the lambda abstraction. The only thing you can do with a lambda abstraction is apply it.
EDIT: In fact I'd guess any function type A -> B where A is infinite cannot be mapped to the naturals.
Internally, in the lambda calculus itself, or a model of it, there are two caveats, however:
(0) Nothing guarantees that all internal inhabitants of a type are denotable by external pieces of syntax. For example, most real numbers are undefinable. (There are only countably many formulas over a finite alphabet, but uncountably many real numbers, ergo, most real numbers can't be “pinned down” using a formula. That doesn't prevent them from existing. The situation is exactly the same with a type like `nat -> nat`.)
(1) The right internal notion of equality isn't syntactic equality (which doesn't even make sense, for the reason stated above), but extensional equality.
If all of this sounds too strange, read more about model theory, Gödel's completeness theorem, and the Löwenheim-Skolem theorems.
Undefinable real numbers exist, whether you can compute them or not.
> and we are talking of models of computation.
A theory of computation that rejects the existence of things that can't be computed is like a logic that rejects the existence of FALSE because it can't be proved. Where does the busy beaver function sit in your conceptual model?
I agree with you, but as you probably know this is a deep ontological question. The meaning of something "existing" has been debated for many centuries, especially for cases such as this.
> A theory of computation that rejects the existence of things that can't be computed is like a logic that rejects the existence of FALSE because it can't be proved. Where does the busy beaver function sit in your conceptual model?
There is a difference between rejecting and classifying. I am not proposing a new computational model. Turing's model classifies the busy beaver function as non-computable. Correct?
I thought we were discussing Church-Turing. This assumes Turing Machines, and what they can compute. Of course you can break everything by assuming an imaginary machine that can compute functions that are not computable by Turing Machines...
> I thought we were discussing Church-Turing. This assumes Turing Machines, and what they can compute. Of course you can break everything by assuming an imaginary machine that can compute functions that are not computable by Turing Machines...
Turing never redefined the concept of “countable”, which belongs in set theory. If you had asked him what the cardinality is of the set of functions from the naturals to the naturals, he would've answered you “uncountable, of course”.
This seems trivial to prove: any function representable in any given programming language maps to a finite string of characters, and finite strings of characters maps to natural numbers.
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.
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.
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.
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 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.
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.
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. 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). 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.
: 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).
: I'm skeptical because I believe we're close to the "Brooks limit": http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...
> 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).
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.