Hacker News Reader

Comment by marshray | Hacker News Reader

It sounds like he had a productive day learning, but from the article it's not clear that he came away with a real appreciation for the fundamental difference between (HTML and CSS) and Javascript.

I may be biased, but to me the verb "to code" means implementing things that require Turing completeness to express.

View on HN

There are some neat advances in Programming Language research, relating to restricting languages (or sub-languages) to a terminating subset. This is typically done in a functional context, and then you can do this by restricting recursion.

These non-turing-complete languages can be used for some useful things, besides the compiler's proof that they terminate. The main use is getting totality (knowledge that for all valid inputs, you will get a valid output) and then writing programs that generate proofs. The fact a valid, total program that generates the proof exists, means that the proof exists, and we don't have to run the program! Thus, in this terminating-language context, a valid program that generates a proof, is itself a proof.

This is very useful for compiler-verified proofs of correctness about various aspects of your program.

tl;dr: Turing Completeness is taken for granted, but for many kinds of programming, it appears it may be useful to have less.