Мягкое введение в Coq: начало

[@mwizard]

А как верифицировать программы, написанные для Coq? Т.к. они пишутся людьми, в них же тоже возможны ошибки, которые нужно исключить?

[@ymn]

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

[@mwizard]

Формальное описание — это же и есть программа для Coq, верно? Если в формальном описании есть ошибки, то смысл верификации программы пропадает — но как гарантировать то, что их нет? Иными словами, кто будет проверять проверяющего? :)

Честно говоря, я пошел читать про формальную верификацию в Википедии и окончательно запутался в том, что же она, собственно, из себя представляет и как ее применить применительно к более «бытовым» сценариям. Вы не могли бы, например, в следующих статьях (или в комментариях, если ответ тривиален) показать, как именно можно верифицировать стандартный C-шный Hello World?

#include <stdio.h>

int main(int argc, char *argv[]) {
    printf("Hello, world!\n");
    
    return 0;
}

[@ymn]

Конечно, я к этому и веду потихонечку. Сначала надо рассказать про некоторые основы.

[@mwizard]

Тогда ждем следующих частей, спасибо.

[@VoidEx]

Есть надежда на то, что формальное описание проще для понимания (так как декларативно), а может быть ещё и короче.
К примеру, есть верифицированный компилятор C на Coq. В принципе, там могут быть ошибки, они и в самом стандарте могут быть.

[@safinaskar]

То, что вы называете «программами для Coq» — это не программы, а доказательства, записанные на языке Coq. Coq — не язык программирования. Доказательство на Coq нельзя исполнить, но его можно проверить. Проверить при помощи, собственно, Coq, или, что то же самое, чекера (checker) Coq. Т. е. Coq (он же Coq checker) — это такая программа, которая проверяет доказательство, записанное на языке Coq. Единственное назначение доказательства на Coq — это быть пропущенным через Coq checker.

На практике при записи доказательства на формальном языке (таком как Coq) в IDE (хоть Coq и не язык программирования, но среда для удобной интерактивной записи доказательств на Coq называется IDE) checker обычно постоянно запущен в процессе записи доказательства. Не знаю, как конкретно обстоят дела в Coq, но у меня в Isabelle/HOL (ещё один язык для записи доказательств) процесс происходит так: я набираю доказательство на Isabelle/HOL в специальном IDE, checker при этом всегда запущен в фоне, и если что-то не так, проблемное место подчёркивается красным.

Видимо, это и имел в виду ymn, когда написал в посте выше «Если программа содержит ошибки, то это сразу станет ясно». Т. е. если исходная программа на каком-нибудь языке программирования (C, OCaml, Scheme, Haskell) содержит ошибки, то при попытке записи формального доказательства (на языке Coq) её правильности, IDE «подчеркнёт проблемные места красненьким».

Формальное описание — это же и есть программа для Coq, верно?

Нет. Есть три «штуки»:
1. Исходная программа (на C или любом другом языке программирования, которую мы хотим проверить).
2. Спецификация этой программы, написанная на формальном языке Coq, или, что то же самое, формальное описание исходной программы (а лучше даже сказать не «формальное описание программы», а «формальное описание задачи, которую программа должна решать»). Т. е. на формальном языке записываем, что «программа должна делать то-то и то-то». Т. е. формулировка математической теоремы о том, что программа соответствует своим требованиям, т. е. математическая формулировка требований к программе.
3. Собственно, доказательство того, что программа правильная, т. е. доказательство упомянутой выше теоремы, т. е. доказательство того, что программа соостветствует своим требованиям, своему формальному описанию, т. е. спецификации.

Упомянутое вами «формальное описание» — это пункт 2, а то, что вы называете «программой на Coq» — это пункт 3.

Никакой проблемы курицы и яйца тут не возникает. Т. е. не нужно думать, что мы проверяем одну программу другой, её — третьей и т. д. Нет. Есть исходная программа (1). Мы пишем формальное доказательство (3) того, что она соответствует своим требованиям (2). Это доказательство (3) проверяется Coq'ом. И, собственно, всё. Стоп. Никакой дальше бесконечной рекурсии нет. Единственное, в чём тут можно усомниться — это в том, что сам checker Coq действительно правильный, и что проверка доказательства (3) Coq'ом действительно гарантирует его правильность

[@k06a]

Язык ГАЛИНА придумали в институте ИРИНА…

[@Tazman]

Coq — очень крутая и интересная штука. Сам очень люблю подоказывать чего-нибудь, поломать голову. После него Haskell кажется детской игрушкой. Единственный недостаток, найти ему промышленное применение очень сложно. Я периодически поглядываю вакансии, не требуется ли кому-нибудь coq-программист, и пока ничего не нашел, к сожалению.

[@ymn]

Просто Coq-программист скорее всего никому не нужен. Нужны специалисты со знанием предметной области. Например, если вы знаете Verilog/VHDL, то можно попробовать устроиться в Intel или Altera. Если же вы специалист в криптографии, то можно попробовать пробиться в исследовательские лаборатории при зарубежных институтах.

[@Tazman]

Похоже, что так и есть. Вроде даже видел какие-то вакансии, связанные с Verilog/VHDL, где-то в Питере. На сколько я понял, это что-то связанное с проектированием микроконтроллеров и доказательство их корректной работы. Конечно, хотелось бы работать с чем-то более высокоуровневым.

[@roman_kashitsyn]

По первой статье сложно получить какое-либо впечатление о языке и его возможностях практического применения. Пока я вижу только

enum day {Sunday, Monday, Tuesday, Wednesday, Thursday, Friday, Saturday};

static const day NEXT_WEEKDAY[] = {Monday, Tuesday, Wednesday, Thursday, Friday, Monday, Monday};

day next_weekday(day d) { return NEXT_WEEKDAY[d]; }

ASSERT_EQ(Tuesday, next_weekday(next_weekday(Saturday)));

[@roman_kashitsyn]

Назовите хотя бы две, мне ведь интересно.

[@FeelUs]

Похоже это перевод softwarefoundations.cis.upenn.edu/lf-current/Basics.html
со скриншотами