4 ms·

> So, let's make an odd_int_less_than_20587 type and a billion of other types? Yes, what's wrong with that ? Every variable's type should be defined as precise

> So, let's make an odd_int_less_than_20587 type and a billion of other types? Yes, what's wrong with that ? Every variable's type should be defined as precisely as possible when meaningful, that's the whole point (and C/C++ not easily allowing to do that is one of their biggest drawbacks imho.)

cle 5y ago
There's a tradeoff around strictness of nominal types and evolvability, e.g. changing the threshold on such a strict type would be a breaking change.
- yakubin 5y ago
  Changing the threshold without signaling the change in the type system is also a breaking change. It's just that your compiler won't warn you about it when you inevitably forget to update your code. Instead your code is going to break at runtime.
  - cle 5y ago
    Not necessarily, it depends on what you do with the value.
  - jstimpfle 5y ago
    Obviously if you have at most 8/16/32/64 bit types (only making new types because of physical constraints), you'll have way, way fewer breaking changes than if you try to encode bounds extremely tightly and try to update them whenever you 2 instead of 1 somewhere. In fact most software is designed such that the physical sizes are chosen first, and then the practical bounds follow from that.
jstimpfle 5y ago
Are you seriously asking? Because what I suggested rhetorically would be the death of all your programs for the simple cause that line count would quadruple and you would have to touch half your codebase every time you make a tiny change.
- jcelerier 5y ago
  When I make a change today like renaming a method I just let my IDE apply it to the codebase, why would that be different ?
  - jstimpfle 5y ago
    Because if you change one type to include the number 235498 it will also affect 377 other types.
    - jcelerier 5y ago
      why would it ? if you set things such that expected ranges are set where they matter (e.g. where you do arithmetic) you should only have to change the types for which range issues occur, like this (very quick and dirty, likely wrong, but you get the idea): https://gcc.godbolt.org/z/4v6dW9czP https://gcc.godbolt.org/z/4v6dW9czP
      - jstimpfle 5y ago
        Not to hurt anyone's feelings but no I don't get the idea. I find this irritating and very unconvincing. So much work and boilerplate to prove peanuts. Have you ever seen anyone doing serious software development like that? I mean, not just toy examples of some 10-line bean counting program blown up to 100 lines. > void foo(ranged_int<1, 5> a, ranged_int<3, 7> b) Why would I _ever_ write a function like that? Practical proofs need to be about runtime values, not just constants and types. They also need to put multiple values in relation. They need to handle type casts and many more things. Constant integer ranges might be of some use but it's a tiny fraction of the invariants that a programmer juggles in practice, and the source code is already blown up out of proportion just for these ranges. This thing is just not gonna fly. Just multiply some "good" values a few times and there is no way that you can statically prove that the result is going to be in the range as well, even though it might always be the case due to how the values combine each time (simple example: offset + size that the code checked to be within array bounds). Invariants in practice are relations over the runtime values of multiple variables. The focus on single values is basically already where types fail as a correctness tool.

cle 5y ago

There's a tradeoff around strictness of nominal types and evolvability, e.g. changing the threshold on such a strict type would be a breaking change.

yakubin 5y ago
Changing the threshold without signaling the change in the type system is also a breaking change. It's just that your compiler won't warn you about it when you inevitably forget to update your code. Instead your code is going to break at runtime.
- cle 5y ago
  Not necessarily, it depends on what you do with the value.
- jstimpfle 5y ago
  Obviously if you have at most 8/16/32/64 bit types (only making new types because of physical constraints), you'll have way, way fewer breaking changes than if you try to encode bounds extremely tightly and try to update them whenever you 2 instead of 1 somewhere. In fact most software is designed such that the physical sizes are chosen first, and then the practical bounds follow from that.

jstimpfle 5y ago

Are you seriously asking? Because what I suggested rhetorically would be the death of all your programs for the simple cause that line count would quadruple and you would have to touch half your codebase every time you make a tiny change.

jcelerier 5y ago
When I make a change today like renaming a method I just let my IDE apply it to the codebase, why would that be different ?
- jstimpfle 5y ago
  Because if you change one type to include the number 235498 it will also affect 377 other types.
  - jcelerier 5y ago
    why would it ? if you set things such that expected ranges are set where they matter (e.g. where you do arithmetic) you should only have to change the types for which range issues occur, like this (very quick and dirty, likely wrong, but you get the idea): https://gcc.godbolt.org/z/4v6dW9czP https://gcc.godbolt.org/z/4v6dW9czP
    - jstimpfle 5y ago
      Not to hurt anyone's feelings but no I don't get the idea. I find this irritating and very unconvincing. So much work and boilerplate to prove peanuts. Have you ever seen anyone doing serious software development like that? I mean, not just toy examples of some 10-line bean counting program blown up to 100 lines. > void foo(ranged_int<1, 5> a, ranged_int<3, 7> b) Why would I _ever_ write a function like that? Practical proofs need to be about runtime values, not just constants and types. They also need to put multiple values in relation. They need to handle type casts and many more things. Constant integer ranges might be of some use but it's a tiny fraction of the invariants that a programmer juggles in practice, and the source code is already blown up out of proportion just for these ranges. This thing is just not gonna fly. Just multiply some "good" values a few times and there is no way that you can statically prove that the result is going to be in the range as well, even though it might always be the case due to how the values combine each time (simple example: offset + size that the code checked to be within array bounds). Invariants in practice are relations over the runtime values of multiple variables. The focus on single values is basically already where types fail as a correctness tool.