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

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