"Unfortunately, I don't think type theory has a whole lot to do with programming or software engineering. The most practical languages (as measured by popularity, which seems to be the best way to do it over a period of decades) do not have sound type systems, nor even particularly interesting ones theoretically."
That is hilarious! I just showed this to my black, British cat, Mr. Fluffer Wickbidget, III, and he spit out the milk which he had been lapping from the palm of my hand.
You should sit down with the brilliant Hongwei Xi, the creator of the amazing ATS programming language, and see what he thinks of your jocular comment. If you're lucky, he might explain to you the reality of his Applied Type System, which not only provides for a very practical use of types, with the side benefit of theorem proving, but has also been shown to be almost as fast as C.
You seem to think that I think that the problem with languages with powerful type systems is that they are slow, and showing something as fast as C is a proof against this? I don't think your comment is relevant to the thrust of what I wrote, sorry.
That is hilarious! I just showed this to my black, British cat, Mr. Fluffer Wickbidget, III, and he spit out the milk which he had been lapping from the palm of my hand.
You should sit down with the brilliant Hongwei Xi, the creator of the amazing ATS programming language, and see what he thinks of your jocular comment. If you're lucky, he might explain to you the reality of his Applied Type System, which not only provides for a very practical use of types, with the side benefit of theorem proving, but has also been shown to be almost as fast as C.
http://www.ats-lang.org