Z3 можно взять оракулом, нельзя судьёй

Частый совет со стороны: «подключите SMT-решатель и закроете фронт критики». Наполовину верно и наполовину опасно.

Опасно потому, что Z3 — большой внешний решатель. Довериться ему значит доверить корректность двумстам тысячам строк чужого кода. Coq и Lean этого не делают намеренно: у них маленькое ядро, которому доверяют, и всё остальное перепроверяется.

Верно потому, что предлагать доказательства решатель может отлично.

Правильная архитектура у нас уже есть: proof-search-must-trust-nothing — поиск предлагает, ядро перепроверяет. В неё Z3 встраивается как ещё один источник гипотез, и ничего не портит.

Что потеряли бы, взяв его судьёй: ровно то, что отличает flang от остальных — zero-axioms и маленькое проверяемое ядро.

Связано: proof-search-must-trust-nothing, zero-axioms, what-the-popular-stories-get-wrong