> At code level, you should be able to describe your problem in lots of details, use identities to simplify your logic, but leave the optimizations to the compi

> At code level, you should be able to describe your problem in lots of details, use identities to simplify your logic, but leave the optimizations to the compiler. 1. As far as I'm aware, Haskell isn't able to do any of that at the code level. I'm interested in what a language that is able to do that would look like. 2. I'm curious as to what you consider an "optimization" to be left to the compiler, and what you consider part of the "problem". For example, does the compiler decide which implementation of a set to use? 3. I'm also wondering what you mean by "proving correctness." If you're alluding to formal verification, then that is notoriously hard to scale, which conflicts with the stated goal of making optimization easier to scale. Some pseudocode would shed light on all these questions.