From time to time I imagine a language that lets you write constraints on your code in the language yourself — kind of like macros but instead of extending the syntax your compiler understands, they would allow you to extend the set of things you could say about your code that the compiler would then understand.
Auditors in E: http://www.erights.org/elang/kernel/auditors/