Is it possible, in principle, to use comptime to obtain Rust-like safety? If this was a library, could it be extended to provide even stronger guarantees at compile time, as in a dependent type system used for formal verification?
Of course, this does not preclude a similar approach in Rust or C++ or other languages; but comptime's simplicity and generality seem like they might be beneficial here.
https://github.com/DutchGhost/zorrow
It's not a complete solution, among other things, because it only works if you use it to access variables, as the language has no way of forcing you.
Researchers have been working on these three things for decades. Yes, “comptime” isn’t some Zig invention but a somewhat limited (and anachronistic to a degree) version of what researchers have added to research versions of ML and Ocaml. So can it implement all the static language goodies of Rust and give you dependent types? Sure, why not? After all, computer scientists never had the idea that you can evaluate values and types at compile-time. Now all those research papers about static programming language design will wither on their roots now that people can just use the simplicity and generality of `comptime` to prove programs correct.