Hacker News Reader

Comment by urbit | Hacker News Reader

Obviously if you have a door that needs to stay open, a thudingly concrete... never mind.

All I would say is, s/types/PL theory. Let's take your statement as true and stipulate that TAPL is in the top 1% of down-to-earthness of books on PL theory. Is it in the top 1% of down-to-earthness books on, say, Java? If not, what does this tell us about PL theory? You have read TAPL, right?

PL theory is a beautiful system and I've never said otherwise. TAPL is also very good at keeping doors open. But so are many things. PL theory is not the theory of programming, any more than TAPL is the doorstop. It is a theory of programming and a doorstop.

View on HN

> Is it in the top 1% of down-to-earthness books on, say, Java? If not, what does this tell us about PL theory?

Yes I have read TAPL, it's sitting on my desk right now. I'm not even sure what you're trying so say, the fact that a book on type system design doesn't have advice on Java* seems perfectly natural to me. A book on goat husbandry doesn't have advice on Rails development. What are you trying to say?

> PL theory is not the theory of programming, any more than TAPL is the doorstop.

This is the strawmen that you're arguing against that seems bizarre to many people. PL theory is not so much about the lambda calculus and Hindley-Milner as it is about applying rigor and discipline to the study of programming languages. And yes, sometimes that involves learning the mathematical formalism.

* Chapter 19 in TAPL actually does have an implementation of Java's type system.

Right, there you are with the definite article again.

What you're asserting is that without this system of rigor and discipline, there can be no other rigorous and disciplined way of defining programming languages. For one thing, this flies in the face of everything we know about the philosophy of mathematics.

I think my way of defining programming languages is pretty rigorous and disciplined. I'll continue to think that until you or anyone can identify some sloppy ambiguities. I note also that my foundation fits on a T-shirt and yours needs a math textbook...

This is exactly the point, you may think your system is rigorous and disciplined but how do you convey that to other people with them having the same degree of certainty that you feel your system has. The answer to that is the proofs and formalization, and that is the essence of what rigor in programming language design is about.

My definition of "rigorous and disciplined" comes from an entirely different world, the world of RFCs.

Here, you can look at my axioms and identify anything unrigorous or undisciplined about them:

https://github.com/urbit/urbit/blob/master/Spec/nock/5.txt

A bunch of people have written compatible implementations from the spec, which is the RFC world's general sanity test.

I think you missed the point of the (poorly phrased) question. I think the intended question was "would the down-to-earthness score of TAPL fall in the top 1% of the down-to-earthness scores of Java books?"

Reply on news.ycombinator.com