Yes, that's exactly the trade-off I've been thinking of. When I program I like to start out writing tests at the start when I don't yet know what properties I should try to enforce. Over time I start finding places where tests aren't good enough, and start feeling the need for more rigorous checking. But by then I've painted myself into a corner with my choice of language, and it's too hard to switch to a more rigorous platform.
In Mu my plan to break this dichotomy between coverage and soundness is to allow arbitrary metadata to be attached to instruction operands. As a result you aren't stuck with the type annotations and checking that I build into the system. You can have arbitrary metadata and will be able to write programs that can deduce and check this metadata to enforce all sorts of properties. Arbitrary checkers feels to me like a generalization of Lisp macros.
Arbitrary metadata is cool. Clojure has arbitrary metadata, which the compiler uses to optimize function performance, but you can use it for other purposes as well:
