Hacker News Reader

Comment by bbminner | Hacker News Reader

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)?

View on HN

I 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.

The 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-u...

The implementation based on the datalog engine was also found to be generally too slow and was replaced with an ad-hoc dataflow algorithm.

Having 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!

Unification 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.

Reply on news.ycombinator.com