[lou1306]

The idea of a "nice" language for SMT solvers is really cool! Off the top of my head, I think Boogie [0] is pretty similar to OP's plan of building a language that reduces to an SMT query, so it may be worth checking out.

However, I'm not sure that LLVM optimizations will really "allow people to write more robust and complex models". I mean, they might help, but they might also make things worse. LVM tries to make code run fast on a Von Neumann architecture, sacrificing the structure of the input program in the process. But, for an SMT solver, preserving structure may be better than optimizing, for a number of reasons (but basically because solver heuristics may find a solution faster given such additional information).

[0] https://www.microsoft.com/en-us/research/project/boogie-an-i...