[pcwalton]

> Decomposing logic using Hoare triplets and properly incorporating assertions as hints to a model checker wouldn't significantly add time to the development process.

Yes, it would.

[nanolith]

I do it today; your assumption that "it would" is incorrect.

    void z(value* x) {
        /* preconditions. */
        MODEL_ASSERT(valid_value_ptr(x));
    
        /* do operation. */

        /* postconditions. */
        MODEL_ASSERT(z_postcondition(a, b));
    }

In practice:

    z(NULL); /* model failure. */
    z(&uninitialized_value_on_stack); /* model failure. */

It works, and the model checker runs in seconds.