> In order to guarantee that an addition will not overflow you need to check that the integer is below a certain value, for example. Or to be sure that indexing an array will not be out of bounds you need to check the index value. For this last case Rust enables out of bounds access checks for Vecs in debug builds, but disables them for release builds.
This is backwards. In Rust, using the indexing operator on an array is a bounds-checked operation; the alternative is the unsafe .get_unchecked method. This is true regardless of debug mode or release mode, and there isn't any flag or configuration variable to override this.
It's integer overflow whose behavior (currently) changes between debug and release mode, where in debug mode it panics and in release mode it's defined to wrap around (and this can be configured as you please via a build flag).
"Rust is not a language that has user-definable refinement types, but you can find some examples of refinements in the standard library, like NonZero and NonNull"
Rust does not have refinement types but Pattern Types are behind a feature flag and will hopefully come soon. Pattern Types are not quite refinement types but they will allow you to define NonZero et al yourself.
I guess F#'s active patterns are refinement types. It's not clear to me whether they are types, but they are used like types, i.e. "that which matches the specified pattern"
About the last part of the post, Ada has asserts if my memory is correct. And Oberon, if it's still alive. And Eiffel with assertions on preconditions and postconditions of routines (functions or procedures.) Probably those features were shared by many other languages that were fashionable some 30 years ago and never became mainstream. Then Java and C++ did to the industry what C did in the 70s/80s and all those features retreated from what developers almost used to what researchers wrote in their papers.
Ada has asserts, but also pre/postconditions and contracts, invariants, type predicates, not null pointers. Most can be checked statically through SPARK ... with some effort.
We can, yes, but we also can forget to code any such condition as well, which is all too common. And for e.g. C the lack of an explicitly supplied by the programmer runtime-check is exactly equivalent to the programmer explicitly stating and pledging that such runtime-check is entirely unnecessary, and even it's trivial to statically check at compile time that this pledge is in fact false, no diagnostics is required.
I was trying something in the line of refinement types in C++ to solve the sequential method (anti)pattern, without success. For example, one would have
ConfiguredThing Thing::configure(....) &&;
Where ConfiguredThing and Thing have the exact same members, so doing
auto y = std::move(x).configure(...);
would not copy any data around. It seemed to work with optimizations on, but then there are no guarantees that it will always be the case.
Ideally one would want RAII, but that is not always possible, in particular when wrapping C libraries that may have their own logic. Also, the object could be in different states, with different methods available in each state, and then it would be possible to prevent errors at compile time.
The last section, "Checked bending of the rules" seems pretty similar to C++ contracts[0], though the behavior on violations looks like it will be able to vary wildly between consteval and regular contexts, and whether it terminates the running program with a contract violation handler.
Refining a Vecs invariants from program flow is interesting. I'm not sure if it's a good thing or not. It hides an interaction between references and dynamic container types, possibly "protecting" the programmer from understanding the semantics of the program.
I also don't see in this particular case why the reference would be taken before the potential resizing push but used after the push. Maybe with a clearer use-case I could see the point?
This would also introduce dynamic checks at compile time, since you need to run the program in order to compile it now, as the overload selection/precondition depends on the runtime state of the Vec. This necessarily requires a less-strict compilation/interpretation mode to be run before the borrow checker/other static analysis is done, since the static analysis can't know which function is being called. I suppose this is similar to compile-time programming.
It strikes me also, that you could do all this at runtime if you wanted, simply by manually incrementing length if length < cap and assigning to the newly created spot.
Partly kidding of course, it is a super interesting language. It is probably the only language that ever made me feel out depth and I dabble in a lot of niche languages. Pretty cool stuff!
This is backwards. In Rust, using the indexing operator on an array is a bounds-checked operation; the alternative is the unsafe .get_unchecked method. This is true regardless of debug mode or release mode, and there isn't any flag or configuration variable to override this.
It's integer overflow whose behavior (currently) changes between debug and release mode, where in debug mode it panics and in release mode it's defined to wrap around (and this can be configured as you please via a build flag).