6 ms·
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 b
by marshray 15y ago
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.
- lubutu 15y agoCSS is actually Turing complete: Eli Fox-Epstein used CSS to encode Rule 110, which was proven by Matthew Cook to be Turing complete.
- finnw 15y agohttps://github.com/elitheeli/oddities/blob/master/rule110-grid.html https://github.com/elitheeli/oddities/blob/master/rule110-gr...
- Peaker 15y agoThere 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. See also: Agda, Epigram, Coq.