The OpenNET Project / Index page

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



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

Оглавление

В ядро Linux 6.1 приняты изменения, обеспечивающие поддержку языка Rust, opennews (??), 04-Окт-22, (0) [смотреть все]

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


256. "В ядро Linux 6.1 приняты изменения, обеспечивающие поддержку..."  –1 +/
Сообщение от Аноним (122), 05-Окт-22, 15:21 
Может тебе ещё и от колеса отказаться совсем?
Ответить | Правка | Наверх | Cообщить модератору

258. "В ядро Linux 6.1 приняты изменения, обеспечивающие поддержку..."  –1 +/
Сообщение от Аноним (252), 05-Окт-22, 15:32 
Он не выучил что такое:

1. Безопасный язык программирования
2. Надежный компилятор и ПО.
3. Математическая верификация корректности работы программы.

Вот когда выучит теорию и поймет, что в Rust этого нет и небудет, тогда к SPARK подтянутся.

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

260. "В ядро Linux 6.1 приняты изменения, обеспечивающие поддержку..."  +/
Сообщение от Аноним (260), 05-Окт-22, 15:38 
Он не выучил что такое колесо, такому в школе не учат.
Ответить | Правка | Наверх | Cообщить модератору

266. "В ядро Linux 6.1 приняты изменения, обеспечивающие поддержку..."  +/
Сообщение от Someone (??), 05-Окт-22, 16:54 
SPARK это не "математическая верификация кода", а просто тупо запрет динамического выделения памяти. То есть никаких динамических массивов и т.д.

Математическая верификация это как минимум Haskell

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

271. "В ядро Linux 6.1 приняты изменения, обеспечивающие поддержку..."  +/
Сообщение от Аноним (252), 05-Окт-22, 17:20 
SPARK дает математическую верификацию исходных текстов на предмет отсутствия ошибок работы с памятью и падений во время работы программы. Причем SPARK-2014 делает на конец это просто и удобно.

SPARK - математически верифтцируемое подмножество языка программирования ADA.

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

317. "В ядро Linux 6.1 приняты изменения, обеспечивающие поддержку..."  +/
Сообщение от Someone (??), 07-Окт-22, 19:41 
Ты бы глянул что ли как это математически доказывается.

Да черт возьми даже Idris вместе с Coq будет проще.

К кроме все это доказательство сводиться к статике. Никаких динамически изменяемых массивов!!!

Нафиг такой язык в ядре?

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

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

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




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

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