Using constraint resolvers in programming languages ​​and compilers

Question

Any more or less practical programming language and compiler must deal with limitations. The most common limitation is type. Typically, the type of derivation and unification is performed using a simple algorithm ( Hindley-Milner , where, finally, all terms in the program are assigned a unique type. If this does not happen, an error indication will appear.

Compilers may have more complex constraints, where complete unification is not possible, and a solution exists only under certain constraints. Possible examples:

• Data flow analysis. Solving the constraints of affine equality can be used to vectorize a vector.

• Memory management. If we have some restrictions on links and data access patterns, the compiler can benefit from optimized reference counting and garbage collection.

On the other hand, constraint solvers, such as Z3 or Yices, are very effective at finding acceptable models for different types of constraints.

I am looking for success stories of how compilers benefit from the capabilities of SMT solvers and what tasks they solve. I have listed some areas, but I have not found specific examples. Can you suggest any?

Answer 1

SMT solvers are often used to implement programming languages ​​that require extensive static verification. For example, languages ​​that use dependent types, qualification types, or statically enforced contracts often use SMT solvers.

For example, Liquid Haskell , as well as Microsoft Dafny and Chalice all use Z3. Other languages, such as ATS or Whiley , have implemented their own solver.