Coq 8.12

программы вместе с доказательством соответствия спецификации.

Когда уже они взлетят?

Тащемта уже. Я знаю проект Airbus’а, в котором очень-очень важный софт так пилили. Но геморройно, дорого и долго. Более того, вменяемая спецификация сама по себе таких размеров, что приходится искать ошибки уже в ней.

Есть другая идея: использовать зависимые типы в ограниченном объеме для повышения надежности кода. В этом направлении идет Idris, и мне кажется, что для общего программирования именно что-то такое может взлететь.

А Coq и компания останутся для теорем и критически важного софта.

Ну петухи то как бы не очень летают...

Рождённый ползать — летать не может.

Coq

У того, кто так назвал проект, явно есть coq.

Скорее всего по CoC название Coq неприемлемо )

Ну или ещё француз-патриот.

Более того, вменяемая спецификация сама по себе таких размеров, что приходится искать ошибки уже в ней.

Если спецификацию и саму программу пишут разные люди, то норм

Если спецификацию и саму программу пишут разные люди, то норм

Разные люди не допускают ошибок?

Скорее всего по CoC название Coq неприемлемо )

По CoC (Calculus of Constructions) с названием Coq всё в порядке

Разные люди, как правило, допускают разные ошибки ;)

Например так выглядит доказательство теоремы Пифагора:

Theorem Pythagore :
 forall A B C : PO,
 orthogonal (vec A B) (vec A C) <->
 Rsqr (distance B C) = Rsqr (distance A B) + Rsqr (distance A C) :>R.

Другие примеры можно тут посмотреть: https://madiot.fr/coq100/

Кок – петух, галина – курица.

Это формулировка (тип). Доказательством будет терм, который можно написать явно или построить с помощью тактик.

Тащемта уже. Я знаю проект Airbus’а, в котором очень-очень важный софт так пилили.

Я работал в небольшой компании, где была группа математиков, которая использовала coq для проверки одной из blockchain сетей.

И да, со стороны это выглядело именно так:

Но геморройно, дорого и долго.

:)

Я бы вообще хотел посмотреть со стороны, как это выглядит применительно к софту…