Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Holy Trinity: Logic, Languages, Categories (2011)

existentialtype.wordpress.com

Post reply on HN
Print view View original

11–20 of 51 posts

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#11

Post by posterboy »

throwaway729 wrote: post #9
xchaotic wrote: post #6

How 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 desc…

> > As far as I remember attempts to use proofs in production were counter productive

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.

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#12

Post by throwaway729 »

posterboy wrote: post #11
throwaway729 wrote: post #9

Earlier quoted context omitted.

> 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 desc…

> > As far as I remember attempts to use proofs in production were counter productive 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.

> Wait, does that mean in development?

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.

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#13

Post by dvt »

> Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof!

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

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#14

Post by posterboy »

igravious wrote: post #2

This 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

The second comment in the discussion is confusing. What's the significance of the order in the tuple? An unordered set should be enough, so the tuples would be obvious permutations. Is the order decoded in the elements, eg. the operator *?

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#15

Post by Chinjut »

dvt wrote: post #13

> Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof! 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 lik…

Yes, Bob Harper is aware of, and intentionally discussing precisely, this. (The "Curry-Howard-Lambek" correspondence, if you like)

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#16

Post by jimhefferon »

xchaotic wrote: post #6

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

Certainly it fails the labrador test: you can't eat it.

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#17

Post by dvt »

Chinjut wrote: post #15
dvt wrote: post #13

> Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof! 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 lik…

Yes, Bob Harper is aware of, and intentionally discussing precisely, this. (The "Curry-Howard-Lambek" correspondence, if you like)

He's a PhD in CS so I assumed he did :) I linked it for other people that may not know that it's a thing. The article itself is a bit hand-wavy.

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#19

Post by SomeStupidPoint »

adamnemecek wrote: post #10
lambdasquirrel wrote: post #8

Earlier quoted context omitted.

Probability is an application of this aforementioned math, not foundational to it.

The empirical point of view is definitely worth mentioning.

Could you elaborate on what you mean here? Im not sure I understand what you're trying to say.

Re: The Holy Trinity: Logic, Languages, Categories (2011)

#20

Post by adamnemecek »

SomeStupidPoint wrote: post #19
adamnemecek wrote: post #10

Earlier quoted context omitted.

The empirical point of view is definitely worth mentioning.

Could you elaborate on what you mean here? Im not sure I understand what you're trying to say.

Well fundamentally probability is a framework for reasoning about the future based on previous events. This framework is analogous to logic but it's separate and even though it's not as clean it's a lot more useful for dealing with the real world.
Post reply on HN