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
1
2
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.
That makes more sense. But she makes PL sound like another formal one.
2
1
Yeah "PL" usually refers to programming languages research specifically
1
And it's about how we can potentially build tools based on that work that can work with existing languages. One example of something a bit along those lines (seeing as you mention Ada), is SPARK.
1
2
Cool. (I mentioned ADA because mission critical defense systems are always candidate projects from formal systems.)