3 ms·
Google Godel's incompleteness theorem. In a nutshell, if you can mathematically prove a certain degree of soundness of your code, you have not done anything to
by huahaiy 8y ago
Google Godel's incompleteness theorem.
In a nutshell, if you can mathematically prove a certain degree of soundness of your code, you have not done anything to show your code does what it is supposed to do.
Basically, you could be doing wasted work to satisfy your compiler, and have made zero progress in solving your problem, because that's not what the type system does.
Dynamical languages focuses on solving problems of human beings. The human beings' requirements are often inherently arbitrary, logically unsound, or even self-contradictory. Shoehorning a type system in there often serves to make solving human's problem harder. Consequently, in practice, most popular programming languages are dynamic. The current craze with types is just a fad, in my opinion.
- purple_ducks 8y ago> Dynamical languages focuses on solving problems of human beings > Shoehorning a type system in there often serves to make solving human's problem harder. For the first pass author maybe. Subsequent readings and modifications of the code by other authors are much, much harder without "annotated" code (be that types or schema like spec)
- skuro 8y agoHaving worked on many codebases of all sizes, hand written by an ever changing population of developers (contractors, interns, consulting companies, etc.) I don't look at such annotation as the holy grail of developer-to-developer communication (in this respect, I find them quite less powerful than tests), nor as the philosophical stone of coping with changing requirements.