No subject appears to be more controversial to distributed systems engineers than the oft-quoted, oft-misunderstood CAP theorem. The CAP FAQ— Сейчас я тебе объясню... — Объяснить я и сам могу, ты расскажи, что на самом деле происходит! (Из разговора политологов, но для CAP-теоремы подходит тоже)— Давайте уже запишем CAP-теорему на языке Coq и посмотрим, что там на самом деле. (Я) Читать далее
Продолжаем серию статей о CAP-теореме и языке Coq. В предыдущей части мы детально проанализировали определения CAP-теоремы, готовясь к её формализации на языке Coq, и нашли там серьёзную ошибку (теперь будет о чём поговорить при случае на system design interview).В этой статье мы познакомимся с основами языка Coq и для практики формализуем небольшой фрагмент геометрической системы, близкой к евклидовой. Читать далее
Данная статья является адаптированным переводом моей статьи: Formalization of code in Coq - tactics, написанной в период работы над проектом coq-tezos-of-ocaml. Суть проекта: часть исходного кода протокола криптовалюты Tezos была переведена на Coq, а затем верифицирована с помощью математических методов и…
(картина "лучшего в мире рисовальщика петухов" "Очень одинокий петух" взята с просторов интернета)Сопоставление с образцом в Coq на первый взгляд выглядит не сложнее, чем в большинстве языков программирования, т.е. довольно просто. Правда, это впечатление остаётся только до тех…