4 ms·

Runtime assertions are easily inserted, but why not change the types, make that case impossible? Dependent types can make that happen. Static assertions are en

Runtime assertions are easily inserted, but why not change the types, make that case impossible? Dependent types can make that happen. Static assertions are enabled by dependent typing. But unlike dependent typing, static assertions are only assertions, for example they do not enable you to write a function that returns different types based on its arguments. Static assertions do not allow you to write a compile-time vector type.

AnimalMuppet 6y ago
"Making that case impossible" is hard for i2c not responding. You can represent "not responding" in a way that isn't confused with real data (even if zero-length), and you can refuse to go down the path that expects data. But no dependent type can make it respond. And you're still stuck with the questions: "What do I do then? How do I handle it? Can my program continue at all? How do I tell the user what's wrong?" As far as I can see, dependent types don't help with the larger problem at all.
- lmm 6y ago
  Types (you don't even need full dependent types) let you check your reasoning about why something is true, which is IME the core of the larger problem. Most of the time the bug doesn't happen because everyone forgot that it's possible for i2c to not respond, it's because component a thought that it should pass the i2c response straight through to component b and component b would handle the i2c not responding, whereas component b thought that component a had already handled the case where the i2c didn't respond (or rather, component b is a pass-through middleware that calls component c that wraps component d and component d thought that i2c not responding had already been handled). Types absolutely help with that.
hansvm 6y ago
Plausibly, there could be plenty of cases for favoring runtime assertions over dependent types. Or for mixing and matching even in cases where one or the other would probably suffice. - Dependent types aren't easily available everywhere. If you don't have them then you can't use them. - The compiler can't prove some statements (admittedly not a big issue for the examples from TFA). Supposing you have a dependent type system which allows you to state that a property holds, it could still be prudent to have a runtime check. If the type system doesn't allow such statements then it isn't sufficiently expressive to solve the problem in the first place. - Assertions are a local change which one can make incrementally, whereas changing the types being used will immediately require larger changes (if the types are used more than once) or necessitate some extra wrapper code.

AnimalMuppet 6y ago

"Making that case impossible" is hard for i2c not responding. You can represent "not responding" in a way that isn't confused with real data (even if zero-length), and you can refuse to go down the path that expects data. But no dependent type can make it respond. And you're still stuck with the questions: "What do I do then? How do I handle it? Can my program continue at all? How do I tell the user what's wrong?" As far as I can see, dependent types don't help with the larger problem at all.

lmm 6y ago
Types (you don't even need full dependent types) let you check your reasoning about why something is true, which is IME the core of the larger problem. Most of the time the bug doesn't happen because everyone forgot that it's possible for i2c to not respond, it's because component a thought that it should pass the i2c response straight through to component b and component b would handle the i2c not responding, whereas component b thought that component a had already handled the case where the i2c didn't respond (or rather, component b is a pass-through middleware that calls component c that wraps component d and component d thought that i2c not responding had already been handled). Types absolutely help with that.

hansvm 6y ago

Plausibly, there could be plenty of cases for favoring runtime assertions over dependent types. Or for mixing and matching even in cases where one or the other would probably suffice. - Dependent types aren't easily available everywhere. If you don't have them then you can't use them. - The compiler can't prove some statements (admittedly not a big issue for the examples from TFA). Supposing you have a dependent type system which allows you to state that a property holds, it could still be prudent to have a runtime check. If the type system doesn't allow such statements then it isn't sufficiently expressive to solve the problem in the first place. - Assertions are a local change which one can make incrementally, whereas changing the types being used will immediately require larger changes (if the types are used more than once) or necessitate some extra wrapper code.