LINUX.ORG.RU

Coq 8.12

 


2

2

Вышла версия 8.12 (последняя доступная минорная версия на момент написания новости – 8.12.1) инструмента интерактивного доказательства теорем Coq.

Coq включает в себя язык программирования с зависимыми типами Gallina, опирающийся на теорию исчисления конструкций.

Система Coq позволяет разрабатывать как компьютерно-верифицируемые доказательства теорем, так и программы вместе с доказательством соответствия спецификации.

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

>>> Подробности

anonymous

Проверено: Shaman007 ()

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

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

Crocodoom ★★★ ()
Ответ на: комментарий от Crocodoom

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

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

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

anonymous ()

Coq

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

eternal_sorrow ★★★★★ ()

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

Man-o-Jar ()
Ответ на: комментарий от anonymous

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

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

Crocodoom ★★★ ()
Ответ на: комментарий от Crocodoom

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

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

korvin_ ★★★★★ ()
Ответ на: комментарий от Man-o-Jar

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

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

Crocodoom ★★★ ()
Ответ на: комментарий от korvin_

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

Crocodoom ★★★ ()

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

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/

nikolnik ★★★ ()
Ответ на: комментарий от nikolnik

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

keinu ()
Ответ на: комментарий от anonymous

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

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

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

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

:)

X-Pilot ★★★★★ ()
Ответ на: комментарий от X-Pilot

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

hatred ()
Ограничение на отправку комментариев: только для зарегистрированных пользователей