Conversation

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?

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.

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!

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.

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?

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.