И ещё не совсем понял, ты пишешь, что "левые std либы могут кидать исключения в каких-то местах, и поэтому мы не хотим форсить их как noexcept". Но разве кидание исключения не будет таким же нарушением контракта документации и при Throws Nothing? В стандарте написано "Throws nothing", а либа кидает исключение - получается опять non conforming
Там лазейка - нарушение контракта, это UB. При UB может быть всё что угодно.
Но да, позиция шаткая