I've been wondering if you could do something like "gradual typing" with full blown proof (or at least dependent types).