One observation from talking to industrial teams: PL has a lot of cool concepts that get lumped together into the same language or community, and industrial language designers then need to decouple them from features they don't want
Conversation
Programming Langauges
1
3
Unlikely. Her research centers around constructing formal proofs for real software. It includes something like symbolic logic. I don't think she means Propositional Logic either. Almost fits.
1
The thread is about programming languages. And yeah, programming languages are deeply linked to proof systems, as she's posted about in the past: twitter.com/TaliaRinger/st.
Also she's right in this thread so I don't know why we are talking about her like she is not! 👋
Quote Tweet
Curry-Howard says that there is a correspondence between programs and proofs, in that the rules for type checking programs correspond to logical rules.
It's the coolest thing I learned in undergrad. I'll try to explain a little.
Show this thread
But she says, "PL has a lot of cool concepts that get lumped into", this suggested to me shes referring to another formal language. Industry is very familiar with ordinary programming languages: ADA, C, Java, etc. Her COQ is some kind of a proof library?
2
Ahh I think I get the confusion - the thread is about academic programming language research, which is often running a couple of decades in front of most mainstream programming languages.
2
2
Show replies