5 ms·

I'm forever baffled by the complete inability of our industry to see time or care about seeing that our most precious resource is time. One thing is true: if y

I'm forever baffled by the complete inability of our industry to see time or care about seeing that our most precious resource is time. One thing is true: if you're not proving correctness of your code -- formally or informally -- then you are living in entropy and at very high risk of inefficiently delivering value through software. Knowing how to call "correct" on code is paramount. And also -- yes, static type systems allow for (partial) machine verification of these proofs. The missing piece is the innate -- and immense -- cost in having to express these proofs formally in a machine-checkable way. Static type enthusiasts typically downplay these costs but they are simply wrong. I am not talking about the cost of learning how to code in a statically typed system--that should never be factored in. I am talking about the innate costs of formal verification (and strong static typing) that even the expert static typers pay. I have seen these guys work and they are delivering sub-optimally in time compared to the alternatives. Period. I have been around the block with both static and dynamic typing systems and the latter by far optimizes for delivery throughput over time. Formally proving correctness of your program has the upfront cost of formalizing the proof (to the degree required by the verification system) as well has having the effect of crystallizing your code in its current representation which makes it more difficult to (re-)factor for future uses. Some of the (more reasonable) strong static type enthusiasts will concede that this kind of machine/type-proving is better done when the domain and code stabilizes. My hats off to these people for at least being honest about things. However the next realization is that once code and domain stabilize the need/value for machine proving correctness (in typical business/data applications) drops substantially (for obvious reasons). So the pragmatic value of strong type systems and formal verification is far lower than the proponents will have you believe. Of course we've known this truth forever but our industry forgets pretty quickly. Haskell and variants are on the rise in popularity; but make no mistake, if you are optimizing for overall delivery throughput over time -- even experts are swimming upstream with these languages. Of course every time I point this out on HN I get downvoted -- but it kills me to think that a next generation of programmers are being misled down a path of formal purity with misrepresentative claims about the cost of using these tools in real business applications. Just to dispel any idea that what I'm saying is philistinic, I am a mathematician/academic first, enjoy category theory, have written more than my share of academic proofs (including novel results), and think these tools are immensely fascinating. But having been in industry now for 20+ years shipping web-scale and distributed data systems for business industries (what 90+% of us are doing, I imagine), where time is the most precious resource, I know with certainty that leaning on formal verification techniques (including strong static type systems) is an enormous tax compared to the alternative. That these tools work against fast-paced, iterative development. It has also become evident to me that there is a vanguard of static type enthusiast who are not admitting (or perhaps do not understand) the relative cost of the pursuit. Who will point to a few null pointer errors (that, mind you, could be eliminated or reduced by other defensive coding techniques besides formal proofs) and use these to justify the herculean cost of their formal system. If you're a junior or on the fence about static type systems - at least code in a weakly typed PL in which you can lean in one way or the other. If business outcome/throughput is what you value first and foremost, I guarantee you will gravitate more and more toward dynamic evaluation - especially as you realize the world of real business delivery produces constantly changing requirements and carrying out delivery in the face of purist formal modeling and proofs will be a substantial drag on what you can do for little relative benefit downtream.

nspassov 7y ago
Thank you for taking the time to write this response.
wellpast 7y ago
I do want to add that no one is off the hook for writing correct, production-stable programs. What I'm saying is that there are other tools and skills that can and must be acquired to deliver quality code at high throughput. Formal proof systems focus on quality at a huge (and unnecessary) expense to throughput/development speed.
zozbot234 7y ago
> However the next realization is that once code and domain stabilize the need/value for machine proving correctness (in typical business/data applications) drops substantially (for obvious reasons). These reasons are not obvious to me or to many proponents of static typing/analysis. There's a lot of 'stabilized' code especially within libraries, that could be endowed with formal guarantees. Whereas plenty of other "business-relevant" code doesn't even come with a formal definition of what it's supposed to do, but "lightweight" static techniques would still be useful if only as a means of avoiding egregious mistakes (no mixing feet and meters in the same calculation, that kind of thing).
- wellpast 7y ago
  The obvious part is that by the time your code stabilizes (and you have good techniques and process) then most of the faults in the code have been eliminated. At this point you should have an informal or formal proof of correctness with little need to take the time to get the machine to do the proof for you. > There's a lot of 'stabilized' code especially within libraries, that could be endowed with formal guarantees. Just to take this a little further consider the many open-source libraries out there written in dynamic languages and in use by thousands of production-facing business code. Perhaps there is justification in cases to apply formal techniques, but these libraries are clearly content to use other tools (informal tools, testing, release process, social processes, etc). > "lightweight" static techniques would still be useful if only as a means of avoiding egregious mistakes I'm 100% in agreement with you here. My argument is that static techniques should be looked at as nominal tools and not be put on a pedestal nor placed on the main path of continuous delivery and development as the static type enthusiasts have it.

nspassov 7y ago

Thank you for taking the time to write this response.

wellpast 7y ago

I do want to add that no one is off the hook for writing correct, production-stable programs. What I'm saying is that there are other tools and skills that can and must be acquired to deliver quality code at high throughput. Formal proof systems focus on quality at a huge (and unnecessary) expense to throughput/development speed.

zozbot234 7y ago

> However the next realization is that once code and domain stabilize the need/value for machine proving correctness (in typical business/data applications) drops substantially (for obvious reasons). These reasons are not obvious to me or to many proponents of static typing/analysis. There's a lot of 'stabilized' code especially within libraries, that could be endowed with formal guarantees. Whereas plenty of other "business-relevant" code doesn't even come with a formal definition of what it's supposed to do, but "lightweight" static techniques would still be useful if only as a means of avoiding egregious mistakes (no mixing feet and meters in the same calculation, that kind of thing).

wellpast 7y ago
The obvious part is that by the time your code stabilizes (and you have good techniques and process) then most of the faults in the code have been eliminated. At this point you should have an informal or formal proof of correctness with little need to take the time to get the machine to do the proof for you. > There's a lot of 'stabilized' code especially within libraries, that could be endowed with formal guarantees. Just to take this a little further consider the many open-source libraries out there written in dynamic languages and in use by thousands of production-facing business code. Perhaps there is justification in cases to apply formal techniques, but these libraries are clearly content to use other tools (informal tools, testing, release process, social processes, etc). > "lightweight" static techniques would still be useful if only as a means of avoiding egregious mistakes I'm 100% in agreement with you here. My argument is that static techniques should be looked at as nominal tools and not be put on a pedestal nor placed on the main path of continuous delivery and development as the static type enthusiasts have it.