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.
Not as it is (it would require mutating the type's "state"), but hypothetically, comptime could be made to support even more programmable types. But could doesn't mean should. Zig values language simplicity and explicitness above many other things.
Thanks, that's informative. This was meant to clarify the bounds of Zig's design rather than as a research proposal. Otherwise, one might read it as an open invitation to just the sort of demonic meta-thinking that its users abhor.
Somebody implemented part of it in the past, but it was based on the ability to observe the order of execution of comptime blocks, which is going to be removed from the language (probably already is).
Why would the mere existence of some static-eval capability give you that affordance?
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.
For the hardware and architecture nerds, CUTLASS now appears to include support for an INT1 (binary) AND-popcount matrix multiplication, in addition to the XOR-popcount present in Turing.
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.