|
|
|
|
|
|
by cle
3378 days ago
|
|
|
> Formalization and proofing is what MATTERS. If you ain't got that, you're basically just guessing. You're guessing either way. By formalizing and using deductive proof on those forms, you're guessing that your forms correctly model the intended behavior, which gets harder as the forms get more powerful and abstract. You can 100% guarantee the properties that follow from the forms. You can't deductively prove that your forms are the right forms, and that becomes more important--and harder to verify--as the forms get more abstract and powerful. Which is what irritates me about static typing zealots. Static typing is useful in that it provides deductive guarantees, but it's not free and does have tradeoffs and pitfalls. Instead of requiring 100% guarantees of correctness, you can relax it and require sufficient guarantees of correctness, which will enable you to use the same mechanisms to inductively prove more useful things more easily, and allow you to use the same mechanisms to verify more assumptions and properties than is reasonably possible with formal verification. That's a tradeoff that should be considered more often than it is. A primitive example of this is the use of unit tests to replace some of the formal proofs done by type checkers. There are undervalued advantages to writing programs that way--leaning on inductive instead of deductive guarantees of correctness. |
|
|
Now, of course, nearly all systems have many properties that you don't want to enforce by the type system. Proofs are hard work, better do them only where it's easiest or really important.
Yet, most times I hear the phrase "static typing zealots", it comes from somebody that does not have experience with a good type system and is thus completely unable to weight off the work of constructing your types and the one of getting enough tests to be sure your program works.