Небольшое сообщество математиков использует программу Lean для создания новой цифровой базы. Они надеются, что она обеспечит будущее их научной области. Ежедне...

В интересное время мы живем, товарищи! В любой публичной деятельности теперь требуется проявлять изрядную креативность, чтобы обойти все ловушки, лишь бы не заде...

Программистка встроенных RTOS Мария Горбунова с FPGA платой Terasic DE10-Lite В викенд я зашел в кафе Red Rock и встретил там программистку встроенных систем Машу Горбунову. Вообще, у этого кафе в...

Данная статья является переводом моей статьи: Formalization of code in Coq - tactics , написанной в период работы над проектом coq-tezos-of-ocaml. Суть проекта: часть исходного кода протокола...

Данная статья является адаптированной русскоязычной версией моей статьи: Handling fold_left in proofs . Функция fold_left , сворачивающая список, довольно популярна во многих (функциональных и...

Это обзорная статья, в которой очень поверхностно и не подробно рассказывается о том, что такое формальная верификация программного кода, зачем она нужна и чем она отличается от аудита и...

Предисловие Сопоставление с образцом в Coq на первый взгляд выглядит не сложнее, чем в большинстве языков программирования, т.е. довольно просто. Правда, это впечатление остаётся только до тех пор,...

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

У нас есть 3 «теории всего» — научная картина мира (все сводится к законам физики), информатика (все сводится к битам) и фундамент математики (все сводится к логике)....