4 ms·
Question for Zig experts: Is it possible, in principle, to use comptime to obtain Rust-like safety? If this was a library, could it be extended to provide eve
by lmh 4y ago
Question for Zig experts:
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.
- ptato 4y agoNot an expert by any means, but my gut says that it would be very cumbersome and not practical for general use.
- pron 4y agoNot 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.
- lmh 4y agoThanks, 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.
- anonymoushn 4y agoIt is possible in principle to write a Rust compiler in comptime Zig, but the real answer is "no."
- kristoff_it 4y agoSomebody 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). https://github.com/DutchGhost/zorrow 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.
- lmh 4y agoThanks, that's interesting.
- avgcorrection 4y agoWhy 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.