По окамлу есть хорошая литература на русском языке. Однако, я считаю, что знание окамла не обязательно. Гораздо важнее знание некоторых основ математики: теория множеств, логика.
А как сливать изменения в итоговой версии от распределенной команды разработчиков? Как следить за историей изменений и в случае ошибки откатывать версии?
ИМХО, пример работы, описанный в этом посте, раскрывает сильные стороны распределенных систем контроля версий.
Просто Coq-программист скорее всего никому не нужен. Нужны специалисты со знанием предметной области. Например, если вы знаете Verilog/VHDL, то можно попробовать устроиться в Intel или Altera. Если же вы специалист в криптографии, то можно попробовать пробиться в исследовательские лаборатории при зарубежных институтах.
Дело в том, что при формальной верификации доказывается соответствие программы ее формальному описанию. Если программа содержит ошибки, то это сразу станет ясно. Если же формальное описание отсутствует или содержит ошибки, то смысл верификации программы пропадает. Или я не правильно понял ваш вопрос?
Видел вашу статью. Некоторое время назад, когда я начинал изучать зависимые типы и теорем-пруверы, выбирал между Agda и Coq. В итоге выбрал второе: есть как минимум два отличных учебника, плюс Coq более популярен, плюс написан на OCaml и умеет экстрактится в него.
Существует структурная эквивалентность между программами и математическими доказательствами, которая формализуется в виде изоморфизма между типизированным исчислением и логическими системами (изоморфизм Карри-Говарда). Фактически можно построить тип, выражающий сложные математические свойства.
Логика высказываний соответствует простому типизированному лямбда-исчислению, исчисление предикатов — лямбда-исчислению с зависимыми типами и т.п.
Более подробно о теории типов можно почитать в великолепном учебнике «Типы в языках программирования» за авторством Б. Пирса.
ИМХО, пример работы, описанный в этом посте, раскрывает сильные стороны распределенных систем контроля версий.
Очевидно, вы некомпетентны в этой области. За сим дискуссию прекращаю.
cabal install yesod-platformЛогика высказываний соответствует простому типизированному лямбда-исчислению, исчисление предикатов — лямбда-исчислению с зависимыми типами и т.п.
Более подробно о теории типов можно почитать в великолепном учебнике «Типы в языках программирования» за авторством Б. Пирса.