The MetaOCaml example is certainly interesting but what it does is increase speed, not reliability. In this case, the type (in some general sense) of n is known at compile time, so the compiler can guarantee that whatever is generated at runtime conforms to that type.

But that's not the type of meta programming that depends on runtime discovery of entirely new information, say, an ORM that discovers changes in the database schema. That's the type of meta programming that made Rails so popular and productive (and slow) for some cases. Obviously, it is impossible to provide compile time guarantees about something that is unknown at compile time.

But I tend to agree with you that it is desirable to have correctness proofs at compile time wherever possible.