..would conditions then become part of a function type? Functions/closures can be arguments to methods.. And so conditions can be in co- or contra-variant position.
In the proposition I made, the only action required by the compiler is to not repeat the assertion, when using the exact same predicate and thus explicitly not part of the type system. The goal was to allow dead simple conforming implementations. This means that generating assertion at the top/bottom of the function is probably already enough, assuming that the optimizer is able to remove duplicates, across function calls. Otherwise all pre and post conditions can be generated in the caller, which make the de-duplication of assertion even easier. Of course a smart compiler could propagate those assertions in the type system, or any kind of AST decorations, use them for optimization, smartly decide between generating them at caller or callee side, … but it is not required to do so.