Optimizations for custom hardware should be derivable automatically, from a series of deductions or program transformations. Like proofs. We start with a model of the hardware. The model would need to describe both the functionality and the performance of the hardware. Then we run some automatic exploration of optimizations. We won’t necessarily get out a proof, i.e. the steps that produce the optimization, but at the very least we will automatically discover the optimization, and trust that, if our model is correct, then so is the optimization itself. And if proofs can be generated (e.g. with proof generation in egraphs), this provides human-readable explanations for the optimizations.