3 ms·

>rather than merely apply mathema^H^H^H^^H^H^H^H logical operations within constraints. This is what all programming and software engineering is - logical oper

>rather than merely apply mathema^H^H^H^^H^H^H^H logical operations within constraints. This is what all programming and software engineering is - logical operations within constraints. Types make those constraints more explicit, and make them work for you rather than against you. They make refactoring of large-scale systems more tractable and less painful, which is invaluable when requirements are shifting. And they can eliminate entire classes of errors, bugs, and security vulnerabilities at compile time, which is invaluable in a day and age when everything is getting hacked. As type systems become increasingly sophisticated, those benefits become even more true. And when you take into account all the man hours spent on a system, not just in building the quick and dirty initial prototype, but in debugging it for production, and then maintaining it over a long period of time with eventually 100% turnover of the initial dev team, then types reduce time and effort spent too. You should read the famous paper Out of the Tarpit. Type systems are one of the best solutions to the tarpit of complexity that large systems inevitably incur. http://curtclifton.net/papers/MoseleyMarks06a.pdf http://curtclifton.net/papers/MoseleyMarks06a.pdf

MaxBarraclough 5y ago
> Type systems are one of the best solutions to the tarpit of complexity that large systems inevitably incur. (Disclaimer: I haven't read the paper you linked.) Also, type systems aren't the only game in town, but they're more approachable than the alternatives. Type systems are a walk in the park compared to formal verification frameworks, for instance. If you write your project in verified SPARK, the prover will take all the guess work out of the interactions between subsystems, but again, verified SPARK is no cakewalk. If your ambitions are no higher than throwing together a giant ball of mud that's impossible to precisely reason about, then sure, stick with an anaemic static type system or a dynamically typed language. As a discipline though, we have the means to do better. (Are my biases showing?) As I mentioned in my other comment, various modern statically typed languages have decisively eliminated null-dereference errors. That kind of thing can't be achieved if the programming environment is a free-for-all. To quote an obscure novel, Nothing is an absolute reality; all is permitted. So it is in the dynamically typed world.

MaxBarraclough 5y ago

> Type systems are one of the best solutions to the tarpit of complexity that large systems inevitably incur. (Disclaimer: I haven't read the paper you linked.) Also, type systems aren't the only game in town, but they're more approachable than the alternatives. Type systems are a walk in the park compared to formal verification frameworks, for instance. If you write your project in verified SPARK, the prover will take all the guess work out of the interactions between subsystems, but again, verified SPARK is no cakewalk. If your ambitions are no higher than throwing together a giant ball of mud that's impossible to precisely reason about, then sure, stick with an anaemic static type system or a dynamically typed language. As a discipline though, we have the means to do better. (Are my biases showing?) As I mentioned in my other comment, various modern statically typed languages have decisively eliminated null-dereference errors. That kind of thing can't be achieved if the programming environment is a free-for-all. To quote an obscure novel, Nothing is an absolute reality; all is permitted. So it is in the dynamically typed world.