Summer of Programming Languages

For anyone who's interested in type theory and programming language foundations and modern development, I've found the talks of these summer schools really interesting and useful. The videos and material are at https://www.cs.uoregon.edu/research/summerschool/summer14/cu... , and you can change "14" in the URL to earlier years to see previous material. It's really a highly valuable set of resources.

> Nowadays serious industrial-strength languages are emerging that are grounded in theory and informed by practice.

This seems a bit overly optimistic, but it's nice to see this kind of positive attitude for a change instead of "Why invent yet another language?".

I am very excited about Swift and I have some respect for what Rust is trying to accomplish, but none of these languages have much foundation in category theory or the ambitious kind of type system that Haskell has been pioneering for a while. And the fact that Go is seeing some traction is a stark reminder that we still have ways to go.

Still, it's nice to see some of these concepts becoming mainstream (lambdas/closures, fold and functional iteration, phasing off inheritance based polymorphism, etc...).

A language shouldn't need to have a foundation in category theory in order to be "grounded in theory and informed by practice."

I think that Bob's (the OP's) is merely saying that the design of languages such as Rust and Swift has been strongly influenced by developers well-versed in type theory (the foundation of programming languages) as well as software development (the point of programming languages) -- this is true for Haskell as well, as he points out, but he is just noting that these well-designed, informed languages are becoming more mainstream.

Also, Rust's type system is more complex than you might expect, involving something called linear/affine types: http://en.wikipedia.org/wiki/Substructural_type_system#Linea...

These languages do have very theoretical foundations even though they might not be readily apparent. ML has a rich theory much of which is applicable to both Rust and Swift's type systems.

This is even more applicable to Rust where the system that deals with lifetimes and ownership are based on ideas that evolved out of linear/affine type systems that can track resource consumption.

Funnily enough linear type systems have a direct connection to linear logic, and via the Curry-Howard-Lambek there is another correspondence to symmetric/closed monoidial categories. Even though sometimes it appears like there is no theory behind these languages, Rust has definitely been aggressively importing some cutting edge thinking from programming languages.

Academics don't care so much about things like programming speed. And the academic environment focusses on proof; a type-safety property will seem much better than a unit test even when both took the same amount of time and have the same practical value.

(For all that, I agree with them though. Maybe the reason programming languages researchers think that is because it's true? Do you have reason to believe they're wrong?)