The OpenNET Project / Index page

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



Вариант для распечатки  
Пред. тема | След. тема 
Форум Разговоры, обсуждение новостей
Режим отображения отдельной подветви беседы [ Отслеживать ]

Оглавление

В ветку ядра Linux-next добавлен код для разработки драйверов на языке Rust, opennews (?), 19-Мрт-21, (0) [смотреть все]

Сообщения [Сортировка по времени | RSS]


75. "В ветку ядра Linux-next добавлен код для разработки драйверо..."  +/
Сообщение от Andrii (?), 19-Мрт-21, 21:44 
unsafe всего лишь флаг, который говорит что в этом месте компилятор не может гарантировать отсутствия багов. Таких мест мало и их легко все grep-нуть и проверить. В то время как C код он весь unsafe (и даже хуже), потому что даже unsafe код rust он намного безопаснее любого C кода.
Ответить | Правка | К родителю #58 | Наверх | Cообщить модератору

77. "В ветку ядра Linux-next добавлен код для разработки драйверо..."  +/
Сообщение от Маняним (?), 19-Мрт-21, 21:50 
Про флаг, грепнуть и тыщи глас мы уже слышали. Если раст ансейф вызывает небезопасный с-код, то почему вызов становиться безопасным?
Ответить | Правка | Наверх | Cообщить модератору

128. "В ветку ядра Linux-next добавлен код для разработки драйверо..."  +1 +/
Сообщение от Аноним (120), 20-Мрт-21, 00:04 
Это математически доказано проектом RustBelt https://plv.mpi-sws.org/rustbelt, вообще в Rust вложено огромное количество усилий для доказательства его корректности и надёжности. Над ним работают сильнейшие научные группы по теории типов и языкам.

Т.е. если у вас есть unsafe, которые оборачивает в безопасные конструкции, то остальной код становится безопасным. Вот это они и доказали.

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

138. "В ветку ядра Linux-next добавлен код для разработки драйверо..."  +1 +/
Сообщение от Аноним (-), 20-Мрт-21, 00:37 
> Это математически доказано проектом RustBelt https://plv.mpi-sws.org/rustbelt, вообще
> в Rust вложено огромное количество усилий для доказательства его корректности и
> надёжности. Над ним работают сильнейшие научные группы по теории типов и
> языкам.

Хрень какая-то с какими-то PhD и прочими теоретиками.
Мы, анонимы опеннета лучше знаем, что там на самом деле и как! Мы все говорим, что раст овно, а значит это правда!1

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

178. "В ветку ядра Linux-next добавлен код для разработки драйверо..."  –2 +/
Сообщение от Аноним (178), 20-Мрт-21, 03:14 
В общем случае доказать "корректность" произвольной программы, написанной на тьюринг-полном языке  невозможно. Это доказал Тьюринг в 1936 г.
см. "Проблема остановки"
https://en.wikipedia.org/wiki/Halting_problem
Rust можно считать тьюринг-полным языком, поэтому автоматическое доказательство "корректности" любой программы написанной на Rust невозможно.
Ответить | Правка | К родителю #128 | Наверх | Cообщить модератору

190. "В ветку ядра Linux-next добавлен код для разработки драйверо..."  +/
Сообщение от Аноним (-), 20-Мрт-21, 03:40 
> В общем случае доказать "корректность" произвольной программы, написанной на тьюринг-полном языке  невозможно. Это доказал Тьюринг в 1936 г.
> см. "Проблема остановки"
> https://en.wikipedia.org/wiki/Halting_problem

1) В общем случае это верно для машины Тьюринга с _бесконечной_ лентой. Только вот у нас в реальности память - конечная, как бы современные вебпогроммисты не пытались уверить в обратном.
> any finite-state machine, if left completely to itself, will fall eventually into a perfectly periodic repetitive pattern. The duration of this repeating pattern cannot exceed the number of internal states of the machine... (Minsky 1967, p. 24)

Ну и да, все возможные варианты программ никому, кроме теоретиков, никуда не упали. На практике интересно подмножество, решающее какие-то реальные задачи.

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

"нельзя доказать в общем случае => значит нелзя доказать для частного случая"
Л-логика.


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

194. "В ветку ядра Linux-next добавлен код для разработки драйверо..."  +/
Сообщение от Аноним (120), 20-Мрт-21, 04:12 
Я вот не стал такой длинный ответ писать. Жму руку!
Ответить | Правка | Наверх | Cообщить модератору

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

Rust к этим языкам не относится, и тьюринг-полноту языка не ограничивают.

>"нельзя доказать в общем случае => значит нелзя доказать для частного случая"
>Л-логика.

Достойный прием - приписать оппоненту свои импликации.

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

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

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


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

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

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

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

457. "В ветку ядра Linux-next добавлен код для разработки драйверо..."  +1 +/
Сообщение от Аноним (457), 23-Мрт-21, 04:44 
> На практике интересно подмножество, решающее какие-то реальные задачи.

А подмножество в котором наш код вызывает kernel panic мы просто не рассматриваем, таким образом наш код 100% корректный.

Г-гении.

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

459. "В ветку ядра Linux-next добавлен код для разработки драйверо..."  +/
Сообщение от Аноним (-), 23-Мрт-21, 15:30 
>> На практике интересно подмножество, решающее какие-то реальные задачи.
> А подмножество в котором наш код вызывает kernel panic мы просто не
> рассматриваем, таким образом наш код 100% корректный.
> Г-гении.

Ну то есть с базовыми понятиями и применимости теории к практие ты не знаком.
Б-балабол.


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

193. "В ветку ядра Linux-next добавлен код для разработки драйверо..."  +/
Сообщение от Аноним (120), 20-Мрт-21, 04:01 
При чём тут проблема останова? Вы читали что там написано?
Ответить | Правка | К родителю #178 | Наверх | Cообщить модератору

314. "В ветку ядра Linux-next добавлен код для разработки драйверо..."  +/
Сообщение от Аноним (-), 20-Мрт-21, 17:14 
> в Rust вложено огромное количество усилий для доказательства его корректности и
> надёжности. Над ним работают сильнейшие научные группы по теории типов и языкам.

Судя по таким заявам - в маркетинг и подмятие экосистем корпами вбуханы сотни нефти, работают лучшие очковтиратели по полосканию мозгов.

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

122. "В ветку ядра Linux-next добавлен код для разработки драйверо..."  +/
Сообщение от Аноним (122), 19-Мрт-21, 23:31 
>даже unsafe код rust он намного безопаснее любого C кода

Мантра.

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

189. Скрыто модератором  –3 +/
Сообщение от Аноним (-), 20-Мрт-21, 03:34 
Ответить | Правка | К родителю #75 | Наверх | Cообщить модератору

Архив | Удалить

Рекомендовать для помещения в FAQ | Индекс форумов | Темы | Пред. тема | След. тема




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

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