4 ms·
I'm not sure you're familiar enough with what a sufficiently powerful type system can accomplish. A full dependent type system is sufficient to statically prove
by gipp 9y ago
I'm not sure you're familiar enough with what a sufficiently powerful type system can accomplish. A full dependent type system is sufficient to statically prove that code meets a given specification. We're not just talking about ints and strings and optionals when we talk about type systems for correct software. See Curry-Howard correspondence.
- blub 9y agoDo I need to know more than what you said - that they can prove that code meets a spec? This can work awesome for small programs and clear algorithms, but as is hinted in the article, one has to first create a correct specification. I gave an example in another post, here's another: unforeseen interactions between two components built to spec.
- planteen 9y agoI completely agree - most often the spec is wrong. For example, it doesn't matter if you have a completely correct implementation of Euler angles for a control system. If gimbal lock wasn't considered in the spec, you are going to have issues.
- sheepmullet 9y ago> I'm not sure you're familiar enough with what a sufficiently powerful type system can accomplish. At what cost? I'd estimate it to be at least 10x development cost.
- kazinator 9y ago> I'm not sure you're familiar enough with what a sufficiently powerful type system can accomplish. A sufficiently powerful type system can compute any partial recursive function at type check time. That's pretty much the upper bound.
- kazagistar 9y agoThe upper bound is arbitrary code, and validating arbitrary proofs.