6 ms·
While I prefer expressive type systems by a long shot, I would be much more careful about it "guaranteeing correctness". Types can act as good documentation an
by aftoprokrustes 2y ago
While I prefer expressive type systems by a long shot, I would be much more careful about it "guaranteeing correctness".
Types can act as good documentation and as a safeguard for stupid mistakes. But the worst bugs are due to logic mistakes, wrong assumptions or non-foreseen corner cases. Here, either types do not help, or designing the type system is so difficult it is not worth the effort, and makes many future changes more difficult.
In my previous company we used Scala (with and without Spark) for everything, and this setup pretty much allows you both extremes. There was always a middle ground to be found, where types were expressive enough that they were useful, but not too much that they came in the way.
- szundi 2y agoIt guarantees certain correctness it is having conversations with you about - this way more correct
- tossandthrow 2y agoJust encode your business logic in types first! Coq, Idris, or F* will certainly get the job done for you! /s
- anonzzzies 2y agoYes, you do if you want to make money on decades timescales instead of some grifter vc 2 year thingy.
- mananaysiempre 2y agoUnfortunately you end up selling your stuff to people building missiles and bombs that way—witness CompCert and Frama-C.
- anonzzzies 2y agoNot us, but yes, you have a point.
- RHSeeger 2y ago> While I prefer expressive type systems by a long shot, I would be much more careful about it "guaranteeing correctness". Yeah, you're not guaranteeing correctness. There's a quote from automated testing discussions that applies here... > You're not proving the system works. You're proving that system isn't broken in specific ways Likewise, for a type system, it's guaranteeing the system is correct for the specific subset of "ways it can be incorrect" that the type system covers.