Recently I have improved a little Rust program using an arena and faster set, going from a run-time of 9 to 4 seconds:
In theory a compiler could perform escape analysis and replace the regular vec allocations with arena allocations, and it could perform a static taint analysis (the taint analysis of this module should show that all the data inserted in the hash is static, so it’s safe https://en.wikipedia.org/wiki/Taint_checking ) to use a less strong crypto but faster set. The program also could use slice-length analysis to allocate the slice only once every loop despite it comes from a zipping of two sub-slices.
I guess doing such optimizations automatically is still far away in the future
I am not sure if I would be comfortable with that level of optimizer cleverness.
The reason why I go towards explicit languages like Rust is to have precise control over what is happening. If I want maximal optimizer black magic which is very good by default but near impossible to tune manually, then I tend to prefer runtime-heavy languages Julia or Java.
I understand, but I think there are some solutions to your problem. Adding to the source code small proofs (written by hand with the help of a proof assistant) that a specific array access is always in-bound is very explicit.
Smart compilers could add optimizations after asking permission to the programmer, and annotating source code if they are accepted, etc
You are right that with (possibly autogenerated) explicit annotations, this would fall back into my comfort zone