AST canonicalisation in arithmetic solvers: https://blog.plover.com/math/24-puzzle-2.html (interesting, I've only seen canonicalisation in compilers previously)
miniblog.
Related Posts
Applying an SMT solver to find missed optimisation opportunities in LLVM's arithmetic tooling: https://blog.regehr.org/archives/1714
Prettier 1.13 has had a ton of polish, but this feature really caught my eye: it explicitly adds parentheses to arithmetic operations, to avoid confusion regarding precedence!
Wuffs: a programming language that prevents null pointer defence, buffer overflow, and arithmetic overflow, all at compile time! Designed for file format parsing.