The OpenNET Project / Index page

[ новости /+++ | форум | теги | ]



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

А в огороде бузина ...


>> автоматическое доказательство "корректности" любой программы написанной на Rust невозможно.
> Достойный прием - приписать оппоненту свои импликации.

Ну-ну.
Достойный прием - сморозить хрень, притянув за уши Тьюринга.

Возможно автоматическое доказательство корректности любой программы - только без гарантии, что множество автоматически доказанных программ будет включать все множество корректных программ.
Впрочем, из "проблемы остановки" следует только (и только) что невозможно создать алгоритм, решающий эту проблему для _всех_ возможных вводов/алгоритмов. Не более.

Ответить | Правка | Наверх | Cообщить модератору

Оглавление
В ветку ядра Linux-next добавлен код для разработки драйверов на языке Rust, opennews, 19-Мрт-21, 20:18  [смотреть все]
Форумы | Темы | Пред. тема | След. тема



Партнёры:
PostgresPro
Inferno Solutions
Hosting by Hoster.ru
Хостинг:

Закладки на сайте
Проследить за страницей
Created 1996-2024 by Maxim Chirkov
Добавить, Поддержать, Вебмастеру