> 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!
> 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.
This is great, I can't wait to be able to use a NonMax type in place of NonZero in a couple of places.
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.
GNAT also has validity checks, which are very, very useful. Fuzzing finds so many bugs with those... https://blog.adacore.com/running-american-fuzzy-lop-on-your-...
Java has had such kind of tooling as addon, thing is most folks don't care.
https://objectcomputing.com/resources/publications/sett/sept...
C++ contracts might finally land in C++26, after missing two revisions, although in a minimal form.
They didn't provide a model checker to accompany the contracts the library provides.
No integration with Java Pathfinder or JBMC?
It's really weird how much they missed the ball.
https://en.wikipedia.org/wiki/Java_Pathfinder
https://www.cprover.org/jbmc/
It's because runtime checking is trivial. We can all code up something to crash-if-condition, or except-if-condition, or log-if-condition.
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.
Some of the ideas are present in other languages beyond those described.
Many do type flow analysis nowadays.
Variant records in Wirthian languages are another approach, although they lack validation regarding accessing wrong active tags.
Ada/SPARK and Frama-C can do refinement on memory addresses.
For refinement types in Rust see e.g.:
https://crates.io/crates/refined_type
https://crates.io/crates/refinement
and
https://crates.io/crates/refined
There are also some interesting optimizations possible around this; see e.g. this discussion on the issue tracker of the latter crate: https://github.com/jkaye2012/refined/issues/9#issuecomment-2...
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.
On a second thought, this may be more in the direction of linear types.
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.
[0] https://en.cppreference.com/w/cpp/language/contracts
If you want to build yet another language then please one that solves this problem...
https://en.wikipedia.org/wiki/Expression_problem
This is the problem that makes being a corporate software developer really really suck.
I agree with you, I perceive it to be really difficult to change existing code to fit new things in. There's all interactions between things.
The source code of the widgets we use everyday - such as text editing or graphical editors are or your web browser's Javascript engine, are enormous.
'Just do X, too' is really difficult with what is already there.
Here you go (not my work, but it's interesting): https://github.com/yzyzsun/CP-next
Do you have an example of the expression problem that can't (yet) be solved in today's programming languages, but could theoretically be solved?
I solved it in mine. I should write a blog post.
I once (tried?) to implement some form of refinement types using C++17 templates as my BSc thesis: https://github.com/frabert/bsc-thesis
It's more or less as horrific as you can imagine...
Nowadays in C++23 land, and with concepts along for the ride, it might be easier, although it begs the question why C++ in first place?
I enjoy abusing C++ templates for fun and for the challenge
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.
> Refinement on memory addresses
This is precisely ATS!
The endboss of programming languages!
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!