On 11-12-28 03:10 PM, Sebastian Sylvan wrote:
So simple logic, special cased for just integers (and maybe some handful of other simple things), but not a full dependent type system. It's ad-hoc, but it may be that some simple "hacks" like this covers the majority of the benefit of dependent types without the complexity of a general system.
This gets Very Hard, much faster than it seems. Recall how small a language has to be before it crosses the decidability threshold; the hacks are very likely to stumble from Presburger into Robinson arithmetic without meaning it. Even if they don't, it's effectively injecting a first-order theorem prover in the middle of the compiler; we don't have the complexity budget in our syntax, semantics, implementation footprint or user cognitive load to begin going there. Our existing typechecker is confusing enough!
There *are* people doing this work, but it's a lot more care required than a collection of hacks, and as Dave says it's very researchy, not a direction we're likely to take Rust. You want ATS or the Boogie verifier on Spec# or something.
-Graydon _______________________________________________ Rust-dev mailing list [email protected] https://mail.mozilla.org/listinfo/rust-dev
