How to Tell a Compiler What We Think We Know?

I have been repeatedly quoted (and tweeted) as having remarked more than once over the last decade, "If it's worth telling yourself (or another programmer), it's worth telling the compiler." In this talk, I will try to explain in more detail what I meant by this. In particular, I have noticed that programming languages provide lots of ways to annnotate one thing, but not very many good ways to talk about relationships among multiple things (other than regard to one as a "server" to which an annotation is attached and the others as "clients"). As a very simple example, we don't even yet have a relatively standard way to say such simple things as "Thus-and-so value is an identity for this binary operation" or "this operation distributes over that operation". Algebraic constraints are one way to express some such constraints, but where in a program should they be placed? How can they be generalized and abstracted? Does object-oriented design make this task easier or harder? I am particularly interested in what we might want to say in the future to a compiler that incorporates a full-blown theorem prover. This talk will be a sort of oral essay, raising more questions than it answers.