Продолжаем серию статей о CAP-теореме и языке Coq. В предыдущей части мы детально проанализировали определения CAP-теоремы, готовясь к её формализации на языке Coq, и нашли там серьёзную ошибку (теперь будет о чём поговорить при случае на system design interview).
В этой статье мы познакомимся с основами языка Coq и для практики формализуем небольшой фрагмент геометрической системы, близкой к евклидовой.