[А вы используете логику Хоара в разработке?]

Я с ней знаком уже пару лет.
Хочу сейчас поделиться размышлениями по данной теме.

Что скрывается за терминами "предусловия", "постусловия" и "инварианты"? Если я скажу, что это та самая штука, которая превращает программирование из гадания на кофейной гуще в инженерную дисциплину, то это не будет преувеличением.

Вот в чём прикол:

1) Ваш код может "работать" и при этом быть полным фарсом
Вы когда-нибудь писали функцию, которая вроде бы делает что надо, но при этом где-то в глубине души понимаете, что она может сломаться в любой момент? Вот это и есть отсутствие гарантий. Логика Хоара говорит: давайте чётко прописывать, при каких условиях функция работает ("предусловие") и что она гарантирует на выходе ("постусловие").

2) Функции - это не чёрные ящики, а контракты
Каждая функция должна чётко заявлять: "Я принимаю вот это, и обещаю вернуть вот это". Если она начинает делать что-то ещё (например, менять глобальное состояние или выбрасывать неожиданные исключения), это как если бы вы заказали пиццу, а получили бутерброд. У меня, кстати, недавно так было - заказывали нагетсы, а получили картошку).

3) Инварианты - это правила, которые нельзя нарушать
Ваш код - это игра с правилами. Инвариант - это такое правило, которое должно выполняться всегда, что бы ни происходило.

Почему это важно?
Потому что когда начинаете мыслить в терминах логики Хоара, вы перестаёте надеяться на удачу и начинаете строить систему, которая действительно надёжна. Это как перейти от "авось пронесёт" к "я знаю, что это сработает, потому что я продумал все условия".

Лайфхак:
В следующий раз, когда будете писать функцию, спросите себя:
- Какие условия должны выполняться на входе? ("предусловие")
- Что я гарантирую на выходе? ("постусловие")
- Какие правила нельзя нарушать? ("инварианты")

Тогда код перестанет быть лотереей и станет предсказуемым, как швейцарские часы.
Но это не точно))