The Holy Trinity: Logic, Languages, Categories (2011)
existentialtype.wordpress.com
The Holy Trinity: Logic, Languages, Categories (2011)
1–10 of 51 posts
Re: The Holy Trinity: Logic, Languages, Categories (2011)
#2This link surfaced on HN before. :)
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
Re: The Holy Trinity: Logic, Languages, Categories (2011)
#3I think that probability also deserves it's place in this tetrad.
Re: The Holy Trinity: Logic, Languages, Categories (2011)
#4I feel like this mystical mumbo-jumbo is counterproductive.
Re: The Holy Trinity: Logic, Languages, Categories (2011)
#5I feel like this mystical mumbo-jumbo is counterproductive.
It's a metaphor and meant to be tounge-in-cheek. There's nothing mystical about the actual content of the post.
Re: The Holy Trinity: Logic, Languages, Categories (2011)
#6How is this going to make my code better?
As far as I remember attempts to use proofs in production were counter productive.
For most systems knowing that print "hello"; will do that is good enough.
Re: The Holy Trinity: Logic, Languages, Categories (2011)
#7An interesting published review of this relationship is "Physics, Topology, Logic and Computation: A Rosetta Stone", by John C. Baez, Mike Stay https://arxiv.org/abs/0903.0340. The first author alos has lots of interesting stuff related to (quantum) computation on his website.
Re: The Holy Trinity: Logic, Languages, Categories (2011)
#8I think that probability also deserves it's place in this tetrad.
Probability is an application of this aforementioned math, not foundational to it.
Re: The Holy Trinity: Logic, Languages, Categories (2011)
#9How is this going to make my code better? As far as I remember attempts to use proofs in production were counter productive. For most systems knowing that print "hello"; will do that is good enough.
> How is this going to make my code better?
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.