Hacker News new | past | comments | ask | show | jobs | submit login

> If a linguistic abstraction prevents you from giving certain classes of wrong instructions, that's very useful, even if the abstraction has no runtime manifestation.

No argument about it. But notice that this applies to programmers, not computers.

The article is about two groups talking past each other because of different terminology. When you say that "programming in the real world is seldom about functions of nat -> nat" you are doing the same, due to badly defined meanings of "programming" and "functions".

> But notice that this applies to programmers, not computers.

It applies to computers, because it's the computer itself that's preventing you from giving it certain classes of wrong instructions. I'm talking about enforcing things mechanically (type checking), not socially (design patterns, best practices, etc.).

As far as the computer is concerned, it is running a nat -> nat function over some data you passed it, and displaying the result.

If you consider that data to be a program, and the resulting messages to be errors, that is completely up to you.

As far as the computer is concerned, a program is just a list of instructions. Not even functions of type `nat -> nat` exist at that level. However, that isn't a very convenient way to program, which is why high-level programming languages exist.

As far as a typed high-level programming language is concerned, a syntax tree that doesn't type check isn't a program, so the question of what it does at runtime is simply ill-posed.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact