Безусловно, существует много ненужных вещей. Вопрос лишь в контексте, о котором идёт речь. По нелепой случайности Хоар популяризовал свои тройки настолько, что все системы верификации помимо остальных механизмов до сих пор используют их. В виде предусловий, постусловий и инвариантов класса. Видимо, так же по недосмотру всё ещё используются инварианты и варианты циклов.
Но раз есть гораздо лучшая замена, буду раз узнать.