The Holy Trinity: Logic, Languages, Categories (2011)
existentialtype.wordpress.com
existentialtype.wordpress.com
505 days ago to be precise during a discussion of the article “Relation Between Type Theory, Category Theory and Logic” on https://ncatlab.org/nlab/show/relation+between+type+theory+a...
Fascinating topic, previous discussion: https://news.ycombinator.com/item?id=9867465
The comment says that you may want to treat the same things in different orders as being the same "thing".
A better, in my opinion, English translation of the univalence axiom is, "identity is equivalent to equivalency" (formally, [(A=B)~(A~B)]). You can find this translation in the HoTT book[0].
Also, check out multisets[1].
[0] http://saunders.phil.cmu.edu/book/hott-online.pdf (PDF page 16, or book page 4)
For those of you that may not know, this is called the Curry-Howard(-Lambek) Correspondence[1]. It establishes an isomorphism between well-formed computer programs and formal logic. This isomorphism is fairly intuitive when doing something like (typed) λ-calculus, but it also applies to things like Java and C++.
[1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
It's also not clear if Curry-Howard is really an isomorphism. For a map to be an isomorphism, structure has to be preserved in both directions, but what is the structure on proofs? That's a wide open question. We can't even agree on what it means for proofs to be equal. (The structure of is the content of Hilbert's 24th problem that he decided not to include in his famous 23 problems [1].) It's better to speak of the Curry-Howard correspondence.
[1] https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_prob...
As far as I'm aware, a complicated, inscrutable, unsound logic is still a logic. It's debatable whether it's a useful logic, but even that's not a fatal flaw for these languages, seeing as their main design focus is making normalisation of programs/proofs convenient.
I suppose the two perspectives of Curry-Howard aren't so much about proving/programming as they are about caring-about-the-theorem/caring-about-the-proof. The existence of non-termination is a problem if you care about theorems, since you can't trust proofs and must deal with them manually to see if they're doing anything fishy.
Java and C++ care so much about proofs that they don't really understand what else you might want to do other than dealing with proofs (programs) manually. If you presented a C++ programmer with an automated theorem prover (given a C++ type signature, return a C++ program fragment of that type) I imagine they wouldn't be particularly impressed, since types are just one small part of the concerns that a C++ programmer has.
unsound logic is still a logic
In the case of C++ and Java, they're not often (ever?) used for proving, yet Curry-Howard tells us that they are logics.
Curry-Howard goes both ways, it's not a reduction of programming to theorem proving; if it were, then we could write optimising compilers for all dynamically typed languages, which output "null" for every input.
Likewise, mathematics cannot be summarised as "getting stuff to compile".
Instead, the concerns and interests of the practitioners from both sides are unchanged by Curry-Howard; it just tells us that both those groups are actually working within the same context, and hence they may be able to share ideas/tools/techniques/etc.
Whilst an unsound logic might be useless to a logician, a programmer (or even computer scientist!) may not care too much, since they might be much more concerned about, say, the computational complexity of an algorithm rather than its types.
Let α → H be a functional type where α is a Person type, and H is a boolean type.
Γ ⊢ α → H Γ ⊢ α
--------------------- (→e)
Γ ⊢ H
A → B
A
∴ B
I was struggling to think of a concrete example less trivial than function application, but I suppose my difficulty just shows how terrible these systems are when viewed as logics (but they're still logics!)
Yep, exactly. Why I think it's hard to think of a more concrete example is because any type theory (like vanilla λ-calculus) is not deductive.
Let me clarify: once you add types to λ-calculus, it (amazingly) becomes deductive! But the type theory itself is not deductive (because types are not tractable, among other reasons).
All them of them are logics. Consistency is not a requirement; it's simply a property a system may or may not have.
I think you're misunderstanding what soundness is. Soundness means that a proof in that logic implies a (semantic) entailment in that logic. That is:
Γ ⊢ A ⇒ Γ ⊨ A
What's the difference between "what is" and "what is already given to us"? What's the difference between codifying and describing it?
This is true even in computer science. Turing machines are sets too! I know, ridiculous.
Harper is saying that the correspondence between logic, language, and category is a suitable foundation for mathematical/logical/computational activity and they're all the same thing. This is not merely in the sense that the objects we work with are given beforehand by some more fundamental theory and we are merely analyzing them, but in the sense that logic/language/category is the appropriate setting in which to define our objects, to do synthetic as well as analytical reasoning. That is what makes a particular theory foundational.
That's like saying that home construction becomes an exercise in atomic physics. Yes, in some sense it's true, but it's so far removed from what's actually going on that it's completely uninteresting.
Take the person working on differentiable manifolds. Do they care about that as problems in set theory? Not at all. Change it to problems in logic/language/category theory? They still don't care. Axiomatize mathematics how you will, they won't care, because they're as many layers away from it as the home construction people are from atomic physics.
Without category theory, certain generalizations of differential geometry would be virtually impossible to describe in any useful matter. These generalizations are extremely important for applications to physics and elucidate a lot of the fundamental structure of the classical theory. Furthermore, you get a much nicer theory when you consider higher geometric structures.
The power of category theory as foundations is that it lets you efficiently study the structure of a theory and how to modify that structure in principled ways.
Sure, the mathematician who is doing hard analysis probably does not care too much about category theory, but every mathematician being educated today knows at least a little category theory because it is the natural setting for certain key mathematical ideas, like cohomology.
In contrast, Set Theory is powerful but it doesn't organize mathematics the way logic/languagecategory theory does.
This blog post is describing a research agenda that has already provided tremendous fruit to language designers. You can find the echoes of this research agenda in the design and implementation of basically every modern typed language, as well as a lot of the infrastructure for dynamic languages.
If you're a language designer and you're not aware of the research agenda described in this blog post, learning more about programming language theory will be immensely beneficial.
If you're not a language designer, then your attitude is kinda weird and off-putting. Like demanding an explanation for how fluid mechanics will make your code better. (As it turns out, understanding the theory behind the languages you're using will make you a better programmer, but that's really beside the point.)
> As far as I remember attempts to use proofs in production were counter productive
You remember incorrectly.
> For most systems knowing that print "hello"; will do that is good enough.
Isn't this attitude exactly how we end up with vulnerability-riddled, brittle, and barely maintainable code? I can't think of a single system I've designed or implemented where all I needed to know was that STDOUT worked properly. Most of my test cases capture far more interesting properties. The more of those test cases my tooling can rule out for me, the better.
Wait, does that mean in development? Otherwise, as I understood production so far it would be dependent typing. Supposedly that infers and automates a lot of otherwise handwritten safety checks.
> You remember incorrectly.
Indeed, Test Driven Development is huge and it's not even really formal. Formalisms should facilitate it a lot.
What you're probably glomming on to is that efforts to push the bounds of what you can prove (higher kinded or dependent types) have had mixed results (mixed in the sense that some people think they're great, others are unconvinced).
So we're in a weird situation where many many people are using a tool, but relatively few are interested in new developments concerning how to use that tool.
I think xchaotic probably meant "in development of production code", and is wrong for two reasons:
1. Compilers are production code, and the research agenda this post describes informs a lot of that code (by way of language design). Unverified compilers still make a lot of use of underlying theory.
2. Correctness proofs and static analyses, which are both deeply related but different from what's being described in this post, are used in production environments every day.