3 ms·

has always been code completion. I disagree. Code completion is overrated and only of marginal importance in the production of high-quality code. The key advan

has always been code completion. I disagree. Code completion is overrated and only of marginal importance in the production of high-quality code. The key advantages of types are: - Enabling ahead-of-time compilation resulting in efficient code. - Guarantees on the absence of specific classes of bugs. (This requires soundness.) - Aiding verification. Types provide a rough classification of program behaviour which drastically simplifies verification. If you don't have types, your program logic needs to make typing information explicit in assertions.

seanmcdirmid 9y ago
1. Nope, as proven that many people use JavaScript in the first place. 2. Type systems have always been super limited in the kinds of bugs they can eliminate, even with "soundness". 3. This sounds like a type theorists point that is completely detached from most programming experiences.
- mafribe 9y ago
  (1) I'm not sure I understand point. JS has long been without alternative, that's why JS has seen such a massive uptake. Moreover all JS alternatives, from TypeScript to Scala.js to Elm to Flow are adding types. Anyway JS's popularity is orthogonal to questions about efficient compilation. Types drastically simplify those, for you can work out at compile time how much memory needs to be allocated for each sub-expression of the program under execution. If you don't have types, you can only do that at run-time, and need extremely complicated JIT compiler technology to make this moderately performant. (2) Sure. Still extremely helpful, all the more so, the bigger the software. If you don't have types to do this, you will have to find those bugs by testing -- much more labour intensive. (3) Detached, maybe, but still true. To paraphrase Sutton's law: I'm detached from the toils of contemporary bread/butter programmers and look at verification because that's where the interesting open problems are.

seanmcdirmid 9y ago

1. Nope, as proven that many people use JavaScript in the first place. 2. Type systems have always been super limited in the kinds of bugs they can eliminate, even with "soundness". 3. This sounds like a type theorists point that is completely detached from most programming experiences.

mafribe 9y ago
(1) I'm not sure I understand point. JS has long been without alternative, that's why JS has seen such a massive uptake. Moreover all JS alternatives, from TypeScript to Scala.js to Elm to Flow are adding types. Anyway JS's popularity is orthogonal to questions about efficient compilation. Types drastically simplify those, for you can work out at compile time how much memory needs to be allocated for each sub-expression of the program under execution. If you don't have types, you can only do that at run-time, and need extremely complicated JIT compiler technology to make this moderately performant. (2) Sure. Still extremely helpful, all the more so, the bigger the software. If you don't have types to do this, you will have to find those bugs by testing -- much more labour intensive. (3) Detached, maybe, but still true. To paraphrase Sutton's law: I'm detached from the toils of contemporary bread/butter programmers and look at verification because that's where the interesting open problems are.