Corrode, проект транслятора из C в Rust, получил финансирование Mozilla

Между типами и доказательствами ещё тов. Карри параллель провёл. Таким образом, эти два утверждения в сумме дают, что механический процесс компиляции раст-кода позволяет доказать непротиворечивость любой теоремы.

Интересный вывод. Только неверный. Для обеспечения безопасности скомпилированного кода, достаточно гарантировать, что каждая компилирующаяся программа представляет собой выводимую теорему в соответствующей формальной системе. Если компилятор отвергнет корректную программу, то это не нарушит безопасности.

Впрочем, если система типов соответствует логике предикатов первого порядка, то согласно теореме Гёделя о полноте, можно сделать компилятор, который скомпилирует все корректные программы и отвергнет все некорректные. Но это неинтересно.

Да. Где теорему Гёделя о неполноте применять-то? Так пока и не ясно.

Если компилятор отвергнет корректную программу, то это не нарушит безопасности.

На второй день индеец Зоркий Глаз заметил, что одной из стен нет. Это совершенно верно. Теперь перечитываем пост про «вычеркните лишний пункт из 4х».

Сначала докажите ваше определение «выразительности»

«Выразительность» — способность писать программы, «интересные» в том смысле, любой (существующий на данный момент) тайпчекер находит в ней false positive ошибки.

имеет какой-нибудь практический смысл. Real-life наблюдений недостаточно. Может теорему Гёделя о неполноте применить? Мммм?

имеет какой-нибудь практический смысл

Многострадальный двусвязный список недостаточно практичен?

Какое слово из «вычеркните один пункт из списка неразумных ограничений, что я привёл» непонятно? Можно написать этот список на safe Rust, несколькими способами. А можно дополнить список теорем доказываемых компилятором Rust'а, сделав свой модуль с этим многострадальным списком.

А можно дополнить список теорем доказываемых компилятором Rust'а, сделав свой модуль с этим многострадальным списком.

Вот это называется «заметать мусор под ковёр».

вычеркните один пункт из списка неразумных ограничений, что я привёл

Я совершенно не знаю Rust (даже в глаза не видел), поэтому затрудняюсь ответить, что нужно вычеркнуть. Могу ошибаться, но все перечисленные подходы либо заметают проблему под ковёр (не безопасно), либо являются вариацией на тему регионов (не выразительно).

Полный аналог сишной структуры (c tail-sharing и прочими маняще опасными штуками) сделать всё-таки похоже нельзя.

Приведите пример того, что нельзя сделать в unsafe блоке в Rust, и что возможно в C?

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

Почему меня должны волновать ваши хотелки?

Вот это называется «заметать мусор под ковёр».

Это. Называется. Вручную. Доказать. Теорему. Что. Всегда. Делают. В. Системах. Интерактивного. Доказательства. Теорем.

Ок, я просто о другом подумал. Если дополнить формальную имплементацию списка пруфом (скорее всего он будет не на Rust ^____~), то да, всё ок.

P.S. Вы выглядите так довольно своей маленькой победой (проистекающей от невнятного объяснения), что это мило ^_____~

Rust fanboys are not the brightest bulbs on the Christmas tree, are they?

Я совершенно не знаю Rust

Ладно, повеселились и хватит. Уровень ваших знаний понятен. Держите ваш список: std::collections::LinkedList

За маняще-опасными хвостами, сами знаете куда идти.

Держите ваш список: std::collections::LinkedList

Первый unsafe на 92й строчке.

Уровень ваших знаний понятен.

Он ничтожен, так же, как и я сам, спорить тут нечего. С гигантами мысли я спорю, только чтобы подтвердить это лишний раз.

За маняще-опасными хвостами, сами знаете куда идти.

Разумеется знаю. Но постарайтесь в следующем треде правильно расставлять сноски. Как правильно — см. выше.

Первый unsafe на 92й строчке.

И? Что вы хотели этим сказать? Вся std чуть менее чем полностью состоит из unsafe. Дальше что?

Вся суть безопасной ржавчины