LINUX.ORG.RU

Вышла бумажная книга «CPDT»

 ,


2

3

Сабж.

Анонс в coq-club:

In case anyone is in the mood to take a break from worrying about the inconsistency of HoTT Coq, here's a quick announcement.

For a few years now, I've been working on a book introducing Coq with an unusual slant, focusing on what I think are the most important techniques to implement and maintain large developments: http://adam.chlipala.net/cpdt/

The book has been available freely online from the start, and I'm pleased to announce that a print version from MIT Press is now available. You can find online ordering links on the page I've referenced.

I'm grateful to MIT Press for agreeing to this experiment where I may continue distributing free versions of the book online.

★★★★★

Спасибо, взял на заметку.

encyrtid ★★★★★ ()

Скачал pdf, полистал, хрень какая-то, это можно как-то применить в работе и получить за это бабла?

DELIRIUM ☆☆☆☆☆ ()

Петушня какая-то

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

Только если ты работаешь в каком-либо Intel, они там такое применяют для верификации железа. Правда, у них HOL, а не Coq.

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

Да ну, какие в ALU бэкдоры? У них после эпических багов жопы болели чрезмерно, вот и побежали остальных догонять.

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

У меня на работе, например, на коке верифицирована подсистема, которая отвечает за ранообразную криптоту, АПВС?

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

Грантик наверно какой-нибудь распилить, больше вроде никак.

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

Этим - никто. На хера, когда есть HOL?

anonymous ()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.