Исходное сообщение
"В ветку ядра Linux-next добавлен код для разработки драйверо..." Отправлено Аноним, 20-Мрт-21 04:16
Есть спец. языки Coq, Idris, Agda... разработанные для доказательства теорем (что благодаря соответствию Карри-Ховарда сводится к "вычислимости" соотв. программ / interactive theorem prove / proof assistant). Так эти языки специально (по дизайну) не являются  полными по Тьюрингу. Rust к этим языкам не относится, и тьюринг-полноту языка не ограничивают. >"нельзя доказать в общем случае => значит нелзя доказать для частного случая" >Л-логика. Достойный прием - приписать оппоненту свои импликации.

Ваше сообщение
Имя*:
EMail:	Для отправки ответов на email укажите знак ! перед адресом, например, !user@host.ru (!! - не показывать email). Более тонкая настройка отправки ответов производится в профиле зарегистрированного участника форума.
Заголовок*:
Сообщение*:	> Есть спец. языки Coq, Idris, Agda... разработанные для доказательства теорем (что благодаря > соответствию Карри-Ховарда сводится к "вычислимости" соотв. программ / interactive theorem > prove / proof assistant). Так эти языки специально (по дизайну) не > являются полными по Тьюрингу. > Rust к этим языкам не относится, и тьюринг-полноту языка не ограничивают. >>"нельзя доказать в общем случае => значит нелзя доказать для частного случая" >>Л-логика. > Достойный прием - приписать оппоненту свои импликации.
	Введите код, изображенный на картинке: