4 ms·
A complete novice question: I think I remember reading that Rust is moving from one of the standard type checking algorithms (this one?) to general purpose Z3 S
by bbminner 2y ago
A complete novice question: I think I remember reading that Rust is moving from one of the standard type checking algorithms (this one?) to general purpose Z3 SMT for speed. Does type checking happen to have the same complexity as SMT? Or Z3 is just so insanely well optimized with heuristics and all that it happens to give better overall performance then problem specific checking algorithms with better theoretical performance (eg this one)?
- deredede 2y agoI think you remember wrong. Rust is moving towards using a datalog engine, but for lifetime resolution (the project is called Polonius), not for type checking. Datalog engines have some similarities with SMT solvers so this might be what you're thinking of.
- Rusky 2y agoThe Polonius rules were formulated using Datalog, but the implementation that will ship in rustc does not use Datalog: https://blog.rust-lang.org/inside-rust/2023/10/06/polonius-update.html https://blog.rust-lang.org/inside-rust/2023/10/06/polonius-u...
- SkiFire13 2y agoThe implementation based on the datalog engine was also found to be generally too slow and was replaced with an ad-hoc dataflow algorithm.
- jahewson 2y agoHaving built a type checker with Z3 in the past, the simple answer to “does type checking happen to have the same complexity as SMT?” is no. That’s because the “T” in SMT, “theories” can be pretty much anything - they’re essentially plugins. A more nuanced answer is that many problems are reducible to SAT, meaning that the answer can technically be yes, but a type checker that simply prints the message “UNSAT” upon failure isn’t very useful!
- RandomThoughts3 2y agoUnification is at the heart of type checking and unification is doable with a SMT solver. So a SMT solver can be a type checker if you want which should show that SMT is indeed much more complex than type checking.