One thing I've wanted to do for a long while is design a language in which one can state proofs of the properties of programs in that language. Not a full-blown theorem prover, just a proof checker, where you have to supply the proof, and the system tells you if it holds or doesn't hold. And not an immensely powerful proof-checker either, just powerful enough to state some simple proofs which hold over an infinite universe of values.
Well, after much thought and sketching, I have come up with a term-rewriting-based proof-checking language called Madison. It supports both direct proof and proof by structural induction, and I have used it to write a proof that the reflection of the reflection of any binary tree is the same as the original tree. It's not much, but I'm quite pleased with it.
Check it out at http://catseye.tc/projects/madison/