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.
2
2
That makes more sense. But she makes PL sound like another formal one.
2
1
That's part of the challenge! There's lots of programming languages out there that don't really have a strong formal basis, and building formal reasoning tools around those can be hard!
2
Part of PL research is working with simpler, more well defined systems, and then using that experience to try and help existing languages out there in the wild in places where they are struggling.
2
1
Like, ideally we'd build languages with a formal basis in mind from the start (see WASM for an example), but that's not the reality… although I hope we can make PL research more accessible, so that we can reach PL implementers earlier at the design time.
Cool? What about something like Scheme? It's old but has some features that might be mathematically appealing?
1
Yeah! Most of the work in this space is around MLs, Haskell, and dependently typed langs, which have common ancestry with Scheme. Typed Racket is a way of adding types and refinements to Racket (a variant of Scheme), which is a bit like what we are talking about too.
1
1
Show replies