А что, люди разучились обобщать свой опыт и передавать его в более сжатой форме? Если Эйнштей 20 лет работал над ОТО, это не означает, что студента тоже 20 лет нужно ОТО учить. Я думаю, 20-30 лет можно уверенно делить на 5. Это во-первых. Во-вторых, если не готовить таких специалистов и не давать им работу, то никакого "совершенно другого" опыта никогда и не возникнет.
Что у нас за вечная обломовщина-то такая? Столько интеллекта и сил тратится на то, чтобы самим себе доказывать, что ничего делать не нужно. Тех же, кто пытается что-то делать, вечно шельмуют. Да хоть истоию Левши взять. И одновременно с этим стоит вечный стон: ой, тут ничего невозможно сделать, надо валить. Так, йопта! Если вы не хотите ничего делать, находя для этого миллиарды обоснований!?
В тех же США совершенно другая изобретательская культура. Если они видят призрачную возможность что-то сделать, то находят миллионы причин это попробовать сделать. Не всегда получается, но они пробуют.
Вот взять бы всех Обломовых, посадить на параход и отправить в вечный кругосветный круиз пускай даже за государственный счёт. Лишь бы не мешали тут дело делать.
Ну, во-первых, это в реалиях современной международной системы разделения труда, которая, вроде как, потихоньку сыпется: см. санкции США против Китая.
А во-вторых, можно же, наверное, как-то рассчитать параметры системы: нам нужно N таких команд для решения задач - и под это построить образовательный конвейр.
Ну, как бы, в промышленности со времён Форда известна технология решения такого рода проблемы: если получение результата занимает много времени, нужно разбить всё на стадии конвейера, и выполнять эти стадии параллельно. В итоге, у нас, допустим, каждый год будет получаться несколько новых господинов Сонгов.
Эффективность конвейра можно рассчитать так, чтобы в экономике было определённое среднее количество таких специалистов каждый год.
Может, имеет смысл строить такую систему образования, чтобы иметь возможность выращивать себе необходимых специалистов? Почему это невозможно? В чём уникальность Лианг Монг Сонга? Почему его нельзя воспроизвести? Кто-то исследовал этот вопрос?
Естественно, я говорю о своём. А что, существуют люди, которые способны говорить о чужом? Но проблема не в этом, а в том, что, как мне кажется, Вы пытаетесь перевести спор на свойства моей личности.
Можете, что-то сказать ещё о технологической невозможности построить систему поверх managed языка? Или диалог исчерпан?
Понимаю. Но разве речь была о том, что разницы нет? Речь была о том, что у тестов есть своя математика.
И термин "безусловное" доказательство несколько неадекватен. Правильнее говорить "логическое", потому что те доказательства, которые Вы подразумеваете, как минимум, обусловлены правилами вывода (которые, кстати, во многих языках, и Rust не исключение, ненадёжные: см. https://counterexamples.org) и набором аксиом, которыми описывается предметная область. И этот набор тоже может содержать ошибки: см., например, баги в CompCert.
P.S. Ну, и, кстати, про тесты тоже есть своя математика, а именно, PCP-теорема. Поэтому противопоставлять тесты и математику, ну, как-то, тоже странно...
А почему не отсутствие UB, о котором каджит писал выше по ветке?
Потому что исходная статья не про отсутсвие UB, а про нулевой runtime? Лично я реагировал на это свойство языка, а не вообще на Rust.
Затем, я отвечал на высказывание о том, что вот теперь-то на Rust мы заживём и начнём писать стабильный код. Будто до появления Rust мы не писали стабильный код. На Erlang, упомянутом Вами, написано довольно много стабильного кода, и на Си тоже. Есть разные способы формальной верификации и обеспечения стабильности кода. И для Си тоже существуют методы формальной верификации. Вот, известный пример: https://frama-c.com/
Тот подход, который предложен в Rust не единственный. Я говорил лишь об этом.
Пункт 3 — начисто игнорирует, например, прерывания (процедура обработки прерывания должна быть как можно более короткой, по сути, ее дело — разгрузить железные буфера, прочитать и записать регистры, и поставить в очередь сам обработчик — пока мусор собирается, сеть теряет пакеты, а ssd простаивает). Да и в целом с работой с железом дружит плохо — и если на x86_64 это можно скомпенсировать частотами (быстрее тормозить), то на Cortex-M0 может просто парализовать функционирование устройства
Почему игнорирует? Наоборот, runtime и сборщик мусора специально так проектируются, чтобы можно было быстро обрабатывать прерывания. Для этого есть специальные решения. Вот небольшой обзор от Google:
Кроме этого, компиляторы языков с автоматическим управлением памятью могут проводить анализ кода и доказывать, что некоторые части кода могут работать без сборщиков.
Кроме этого, некоторые runtime для hard real-time приложений позволяют формировать задачи, которые выведены из-под сборки мусора, с соответствующими ограничениями на допустимый код этих задач.
Кроме этого, можно сразу писать конкурентный код в другой семантике, не в модели последовательного исполнения кода, а, например, в модели realtime-процессов, обрабатывающих сигналы, и тогда многие проблемы разрешаются автоматически.
Я не говорю, что это идеально. Я всего лишь утверждаю, что альтернативные подходы существуют. Достоинство их очевидно - существенно меньшее время разработки. И, недостаток, конечно, очвеиден тоже - нужно очень тщательное проектирование runtime и семантику языка, в которых появляется множество тонкостей, которые нужно согласовать. Но, повторюсь, есть примеры, которые показывают, что это возможно. Вот один из них: https://www.irisa.fr/prive/talpin/papers/fidji03.pdf
За контрпримером даже ходить далеко не надо: вот уже пару недель ядерный kvm регулярно падает после примерно суток работы, жалуясь на списки: указатели, мол, не туда указывают, ни add ни delete не сделать.
Контрпримером для чего? Странно слышать такое от человека, который так горячо приветствует формальные доказательства, и который, гипотетически, должен разбираться в логике первого порядка. Я разве написал, что любая программа на Си стабильна?
Кроме того, в Rust есть проблемы с динамическими структурами данных. Если судить вот по этому (а ничего более полного у меня найти не получается) https://rust-unofficial.github.io/too-many-lists/, даже банальный двусвязный список требует использования unsafe-конструкций. То, что проблемы с реализацией эффективных структур данных есть, подтверждает и чтение исходного кода Redox, в котором структуры данных, мягко говоря, топорные.
Почему Вы уверены, что kvm удастся реализовать на Safe Rust? Я читал исходники kvm, и немного правил их под себя, там используются довольно сложные динамические структуры данных для обеспечения производительности. Можно ли их запрограммировать на Rust с сохранением гарантий?
Важно отсутствие UB
Важна предсказуемость
Важна доказуемость правильности выполнения — не условное покрытие тестами, а математическая верифицируемость
Это, конечно, важно. Но достижимо ли на практике. Можете посмотреть на объём формальных математических доказательств корректности простейших алгоритмов на каком-нибудь Coq, и прикинуть, сколько усилий нужно, чтобы доказать корректность того же KVM. А потом обнаружить, что аксиоматика была некорректной... Вот на примере compcert: https://sf.snu.ac.kr/sepcompcert/compcertbugs/
Впрочем, повторюсь, я говорил исключительно о свойстве нулевого runtime, в том контексте, что это свойство не так важно при разработке системного программного обеспечения, в том числе и для систем с hard realtime требованиями. Повторюсь, подходы к проектированию таких runtime существуют.
Вы слишком быстро жонглируете метафорами. Предлагаю опираться на факты.
Можно ли писать стабильный софт не на Rust? Очевидно, можно, примеров уйма.
Можно ли писать стабильный софт на Си? Можно, примеров множество. Многие примеры летают в космосе. Код на Си можно верифицировать, например, проверкой моделей. Это активно применяется на практике.
Можно ли писать операционные системы на языках с ненулевым runtime? Можно, примеров много. И не очень понятно, как именно runtime усложняет эту работу.
Можно ли писать hard realtime приложения на языках с ненулевым runtime? Можно. Примеров не так много, но они есть, и некоторые подходы выработаны. Есть специальные сборщики мусора, есть техники управления потоками и памятью. Они специфичные, и влияние runtime тут, конечно, нужно учитывать, но я бы не сказал, что это прям вот сильно сложнее, чем программировать realtime-системы на Си.
Итак. Дальше у нас идёт основной вопрос: является ли нулевой runtime значимым свойством языка? Вы же малозначительность этого свойства подвергаете сомнению? Вроде, пункты 1-3 никак не зависят от наличия runtime. Пункт 4... Ну, как бы, с одной стороны, да. Если языку нужен runtime, то при разработке hard realtime приложений возникают тонкости. Но, с другой стороны, runtime может быть заточен под hard realtime задачи, как, например, RTSJ (rt spec for java), и запрограммировать необходимое поведение системы можно.
Соответственно, вопрос: если можно и так и этак, то так ли принципиально важен нулевой runtime? Понятно, что можно постулировать важность чего угодно, хоть макаронного летающего монстра, но есть ли для этого какие-то материальные основания?
Компиляторы Си постоянно тестируют на регрессию огромным количеством тестов, среди которых есть и fast inverse square root. Сомневаюсь, что поломка 20-летнего кода пройдёт незамеченной и окажется для пользователей внезапной.
Гипотетически, такое возможно. Практически, думаю, вероятность такого события настолько близка к нулю, что про Си забудут раньше, чем она реализуется.
Эмс... Я, в основном, высказался о том, что программировать операционные системы можно не только на языках с нулевым runtime... Следовательно, нулевой runtime не является важным свойством для этого.
Из контекста не до конца понятно, мы говорим о принципиальной возможности написать стабильный софт до появления в природе Rust или о цене такой работы?
Вроде как, люди писали вполне стабильный софт даже на ассемблере. То есть, принципиально это возможно.
Вопрос о цене, вроде как, не очевидный. Можно писать эффективные и безопасные программы на языках с ненулевым runtime, и эти языки существовали до появления Rust. И писать на них проще, то есть, дешевле чем на Rust.
Собственно, в итоге и возникает мой вопрос: насколько значимо это свойство нулевого runtime? Оно нужно, чтобы что? Чтобы в ядре можно было программировать? Но в NetBSD можно в ядре программировать на Lua ??♂️
Rust интересный язык, конечно. Я просто пишу о том, что существуют и другие подходы.
Почему в неожиданных, вроде, известно, как программировать, чтобы UB не было? И почему предполагается, что программировать можно было только на C или C++?
А что такое "малопроизводительные"? Мне вот возможностей RK3288@400MHz (потому что плата от Pine64 кривая) хватает для моих нужд: переписка, веб, TeX и программирование. Обсуждаемый Khadas раза а 4 быстрее. Если бы он мог ещё под Linux нормально видео кодировать, чтобы stream-ы с лекциями можно было бы записывать, я бы взял, не глядя.
Именно это свойство — zero runtime — делает Си единственным и безальтернативным кандидатом на роль языка для реализации ядер операционных систем и прошивок для микроконтроллеров. Тем удивительнее, насколько мало людей в мире этот момент осознают; и стократ удивительнее то, что людей, понимающих это, судя по всему, вообще нет среди членов комитетов по стандартизации (языка Си)…
— А. В. Столяров
Нет взаимосвязи между наличием у языка runtime и возможностью реализации на этом языке ядер операционных систем и прошивок для микроконтроллеров. Я знаю о проектах на диалектах Lisp, но, наверняка, есть проекты и на других языках. На Lisp написаны: Mezzano, Loko Scheme, Maker Lisp, LisPi, PilOS, PICOBIT и т.д.
Хотелось бы выразить робкую надежду на то, что пока сообщество Rust самозабвенно борется против C за право занять место царя горы традиционного софта на основании малозначимых свойств языка, где-нибудь в стороне от этой эпической схватки вырастут более изящные системы с более простыми, эффективными, легковесными и разумными API и IPC...
А что, люди разучились обобщать свой опыт и передавать его в более сжатой форме? Если Эйнштей 20 лет работал над ОТО, это не означает, что студента тоже 20 лет нужно ОТО учить. Я думаю, 20-30 лет можно уверенно делить на 5. Это во-первых. Во-вторых, если не готовить таких специалистов и не давать им работу, то никакого "совершенно другого" опыта никогда и не возникнет.
Что у нас за вечная обломовщина-то такая? Столько интеллекта и сил тратится на то, чтобы самим себе доказывать, что ничего делать не нужно. Тех же, кто пытается что-то делать, вечно шельмуют. Да хоть истоию Левши взять. И одновременно с этим стоит вечный стон: ой, тут ничего невозможно сделать, надо валить. Так, йопта! Если вы не хотите ничего делать, находя для этого миллиарды обоснований!?
В тех же США совершенно другая изобретательская культура. Если они видят призрачную возможность что-то сделать, то находят миллионы причин это попробовать сделать. Не всегда получается, но они пробуют.
Вот взять бы всех Обломовых, посадить на параход и отправить в вечный кругосветный круиз пускай даже за государственный счёт. Лишь бы не мешали тут дело делать.
Просто многослойная сборка. В RP Zero память и процессор тоже находятся в одном корпусе.
А что, в мире есть только одна страна?
Ну, во-первых, это в реалиях современной международной системы разделения труда, которая, вроде как, потихоньку сыпется: см. санкции США против Китая.
А во-вторых, можно же, наверное, как-то рассчитать параметры системы: нам нужно N таких команд для решения задач - и под это построить образовательный конвейр.
Ну, как бы, в промышленности со времён Форда известна технология решения такого рода проблемы: если получение результата занимает много времени, нужно разбить всё на стадии конвейера, и выполнять эти стадии параллельно. В итоге, у нас, допустим, каждый год будет получаться несколько новых господинов Сонгов.
Эффективность конвейра можно рассчитать так, чтобы в экономике было определённое среднее количество таких специалистов каждый год.
Философы просто отрабатывают гранты, как умеют... ?♂️ Не думаю, что этот конкретный эксперимент говорит хоть о чём-то...
Может, имеет смысл строить такую систему образования, чтобы иметь возможность выращивать себе необходимых специалистов? Почему это невозможно? В чём уникальность Лианг Монг Сонга? Почему его нельзя воспроизвести? Кто-то исследовал этот вопрос?
Естественно, я говорю о своём. А что, существуют люди, которые способны говорить о чужом? Но проблема не в этом, а в том, что, как мне кажется, Вы пытаетесь перевести спор на свойства моей личности.
Можете, что-то сказать ещё о технологической невозможности построить систему поверх managed языка? Или диалог исчерпан?
Понимаю. Но разве речь была о том, что разницы нет? Речь была о том, что у тестов есть своя математика.
И термин "безусловное" доказательство несколько неадекватен. Правильнее говорить "логическое", потому что те доказательства, которые Вы подразумеваете, как минимум, обусловлены правилами вывода (которые, кстати, во многих языках, и Rust не исключение, ненадёжные: см. https://counterexamples.org) и набором аксиом, которыми описывается предметная область. И этот набор тоже может содержать ошибки: см., например, баги в CompCert.
P.S. Ну, и, кстати, про тесты тоже есть своя математика, а именно, PCP-теорема. Поэтому противопоставлять тесты и математику, ну, как-то, тоже странно...
Потому что исходная статья не про отсутсвие UB, а про нулевой runtime? Лично я реагировал на это свойство языка, а не вообще на Rust.
Затем, я отвечал на высказывание о том, что вот теперь-то на Rust мы заживём и начнём писать стабильный код. Будто до появления Rust мы не писали стабильный код. На Erlang, упомянутом Вами, написано довольно много стабильного кода, и на Си тоже. Есть разные способы формальной верификации и обеспечения стабильности кода. И для Си тоже существуют методы формальной верификации. Вот, известный пример: https://frama-c.com/
Тот подход, который предложен в Rust не единственный. Я говорил лишь об этом.
Почему игнорирует? Наоборот, runtime и сборщик мусора специально так проектируются, чтобы можно было быстро обрабатывать прерывания. Для этого есть специальные решения. Вот небольшой обзор от Google:
https://www.researchgate.net/publication/4075178_A_hard_look_at_hard_real-time_garbage_collection
Кроме этого, компиляторы языков с автоматическим управлением памятью могут проводить анализ кода и доказывать, что некоторые части кода могут работать без сборщиков.
Кроме этого, некоторые runtime для hard real-time приложений позволяют формировать задачи, которые выведены из-под сборки мусора, с соответствующими ограничениями на допустимый код этих задач.
Кроме этого, можно сразу писать конкурентный код в другой семантике, не в модели последовательного исполнения кода, а, например, в модели realtime-процессов, обрабатывающих сигналы, и тогда многие проблемы разрешаются автоматически.
Я не говорю, что это идеально. Я всего лишь утверждаю, что альтернативные подходы существуют. Достоинство их очевидно - существенно меньшее время разработки. И, недостаток, конечно, очвеиден тоже - нужно очень тщательное проектирование runtime и семантику языка, в которых появляется множество тонкостей, которые нужно согласовать. Но, повторюсь, есть примеры, которые показывают, что это возможно. Вот один из них: https://www.irisa.fr/prive/talpin/papers/fidji03.pdf
Контрпримером для чего? Странно слышать такое от человека, который так горячо приветствует формальные доказательства, и который, гипотетически, должен разбираться в логике первого порядка. Я разве написал, что любая программа на Си стабильна?
Кроме того, в Rust есть проблемы с динамическими структурами данных. Если судить вот по этому (а ничего более полного у меня найти не получается) https://rust-unofficial.github.io/too-many-lists/, даже банальный двусвязный список требует использования unsafe-конструкций. То, что проблемы с реализацией эффективных структур данных есть, подтверждает и чтение исходного кода Redox, в котором структуры данных, мягко говоря, топорные.
Почему Вы уверены, что kvm удастся реализовать на Safe Rust? Я читал исходники kvm, и немного правил их под себя, там используются довольно сложные динамические структуры данных для обеспечения производительности. Можно ли их запрограммировать на Rust с сохранением гарантий?
Это, конечно, важно. Но достижимо ли на практике. Можете посмотреть на объём формальных математических доказательств корректности простейших алгоритмов на каком-нибудь Coq, и прикинуть, сколько усилий нужно, чтобы доказать корректность того же KVM. А потом обнаружить, что аксиоматика была некорректной... Вот на примере compcert: https://sf.snu.ac.kr/sepcompcert/compcertbugs/
Впрочем, повторюсь, я говорил исключительно о свойстве нулевого runtime, в том контексте, что это свойство не так важно при разработке системного программного обеспечения, в том числе и для систем с hard realtime требованиями. Повторюсь, подходы к проектированию таких runtime существуют.
Вы слишком быстро жонглируете метафорами. Предлагаю опираться на факты.
Можно ли писать стабильный софт не на Rust? Очевидно, можно, примеров уйма.
Можно ли писать стабильный софт на Си? Можно, примеров множество. Многие примеры летают в космосе. Код на Си можно верифицировать, например, проверкой моделей. Это активно применяется на практике.
Можно ли писать операционные системы на языках с ненулевым runtime? Можно, примеров много. И не очень понятно, как именно runtime усложняет эту работу.
Можно ли писать hard realtime приложения на языках с ненулевым runtime? Можно. Примеров не так много, но они есть, и некоторые подходы выработаны. Есть специальные сборщики мусора, есть техники управления потоками и памятью. Они специфичные, и влияние runtime тут, конечно, нужно учитывать, но я бы не сказал, что это прям вот сильно сложнее, чем программировать realtime-системы на Си.
Итак. Дальше у нас идёт основной вопрос: является ли нулевой runtime значимым свойством языка? Вы же малозначительность этого свойства подвергаете сомнению? Вроде, пункты 1-3 никак не зависят от наличия runtime. Пункт 4... Ну, как бы, с одной стороны, да. Если языку нужен runtime, то при разработке hard realtime приложений возникают тонкости. Но, с другой стороны, runtime может быть заточен под hard realtime задачи, как, например, RTSJ (rt spec for java), и запрограммировать необходимое поведение системы можно.
Соответственно, вопрос: если можно и так и этак, то так ли принципиально важен нулевой runtime? Понятно, что можно постулировать важность чего угодно, хоть макаронного летающего монстра, но есть ли для этого какие-то материальные основания?
Компиляторы Си постоянно тестируют на регрессию огромным количеством тестов, среди которых есть и fast inverse square root. Сомневаюсь, что поломка 20-летнего кода пройдёт незамеченной и окажется для пользователей внезапной.
Гипотетически, такое возможно. Практически, думаю, вероятность такого события настолько близка к нулю, что про Си забудут раньше, чем она реализуется.
В комментарии, на который я отвечал было утверждение, что UB неожиданы. Этому возражал. Вот и вы перечислили места, где проблемы можно ожидать.
Эмс... Я, в основном, высказался о том, что программировать операционные системы можно не только на языках с нулевым runtime... Следовательно, нулевой runtime не является важным свойством для этого.
Из контекста не до конца понятно, мы говорим о принципиальной возможности написать стабильный софт до появления в природе Rust или о цене такой работы?
Вроде как, люди писали вполне стабильный софт даже на ассемблере. То есть, принципиально это возможно.
Вопрос о цене, вроде как, не очевидный. Можно писать эффективные и безопасные программы на языках с ненулевым runtime, и эти языки существовали до появления Rust. И писать на них проще, то есть, дешевле чем на Rust.
Собственно, в итоге и возникает мой вопрос: насколько значимо это свойство нулевого runtime? Оно нужно, чтобы что? Чтобы в ядре можно было программировать? Но в NetBSD можно в ядре программировать на Lua ??♂️
Rust интересный язык, конечно. Я просто пишу о том, что существуют и другие подходы.
Почему в неожиданных, вроде, известно, как программировать, чтобы UB не было? И почему предполагается, что программировать можно было только на C или C++?
А что, раньше не было такой возможности?
А что такое "малопроизводительные"? Мне вот возможностей RK3288@400MHz (потому что плата от Pine64 кривая) хватает для моих нужд: переписка, веб, TeX и программирование. Обсуждаемый Khadas раза а 4 быстрее. Если бы он мог ещё под Linux нормально видео кодировать, чтобы stream-ы с лекциями можно было бы записывать, я бы взял, не глядя.
А сейчас вот смотрю на RK3588
Нет взаимосвязи между наличием у языка runtime и возможностью реализации на этом языке ядер операционных систем и прошивок для микроконтроллеров. Я знаю о проектах на диалектах Lisp, но, наверняка, есть проекты и на других языках. На Lisp написаны: Mezzano, Loko Scheme, Maker Lisp, LisPi, PilOS, PICOBIT и т.д.
Хотелось бы выразить робкую надежду на то, что пока сообщество Rust самозабвенно борется против C за право занять место царя горы традиционного софта на основании малозначимых свойств языка, где-нибудь в стороне от этой эпической схватки вырастут более изящные системы с более простыми, эффективными, легковесными и разумными API и IPC...
S905Y4 - это процессор для ТВ-стиков, вроде, греться не должен... Для этого A35 и нужен, чтобы не дорого, и не грелось.