3 ms·
Type systems are not enough. I'm not sure they're even a good starting point for safety critical software, but they might be good for e.g browsers. You're thin
by blub 9y ago
Type systems are not enough. I'm not sure they're even a good starting point for safety critical software, but they might be good for e.g browsers.
You're thinking at code level, people like Leveson, Knight and others are thinking at system level. The end goal is to have a safe system, not e.g avoid null pointer exceptions through optional types.
- zoul 9y agoOptional types are a good example of how types make a system safer. Sure, they are a pretty low-level guarantee, but that still counts—and if you have an expressive type system, you can make much higher-level guarantees with types.
- blub 9y agoI think they're great! I am pushing to use them in our C++ code base and they empirically do improve safety by transforming UB into a nice exception. But they won't prevent a programmer from using MD5 for RSA signature verification.
- dkersten 9y agoBut if all of these things are correctly typed, then it would be visually more likely for someone to notice that the algorithm doesn't return the type it says. Also, C++ static types are rather weak. Its optional types are useful, but its not like in SML where the compiler ensures that you handled all possible cases. A good type system can't catch all kinds of errors though.
- gipp 9y agoI'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.