I have two questions:
-
András said typechecking dependently typed languages doesn’t really work with static memory allocation and that GC is needed to make it tractable. How does it work in Lean, which is implemented in C++ afaik? Do they use a GC library? If so, then presumably the same can be done with Rust?
-
Is Zig’s comptime (two) staged programming, or are there limitations in expressivity? Or is comptime not built on a solid theoretical foundation? Syntax-wise they seem to be able to get away without splices etc, so I’m wondering if they are cutting corners somehow?