Цифровые нейронные сети очень далеки от реальной архитектуры нейрона. Возможно, чтобы проявлять феномен сознания эта архитектура и не нужна, кто знает? Но реальный нейрон гораздо более сложная штука, чем то, что есть в нейросетях. Более того, реальный нейрон - это физический процесс, с квантовыми эффектами, а не просто арифметическая машина, коим является нейрон цифровой.
Вставлю свои 5 копеек. 2 цента - это если нужно развлечь публику на Хабре. Если же нужен какой-то production, то нужно учесть время, необходимое для разбора того, что сеть нагенерирует. А ошибки там бывают весьма тонкие.
Даже если мы говорим о разработке кода, когда можно всё обмазать тестами или же требованиями привести формальные доказательства корректности, где гарантии, что у сети получится это сделать за конечное время? Особенно в нетиповых ситуациях.
Я так и не смог, например, уболтать Stable Diffusion сгенерировать мне "коней, обсуждающих сферических учёных в вакууме". Думаю, любой начинающий художник за десять баксов нарисовал бы мне такой скетч за полчаса.
Даже Ксавье Леруа допускает ошибки, программируя в Коке https://sf.snu.ac.kr/sepcompcert/compcertbugs/. Куда уж нам, простым смертным? Всегда можно накосячить в аксиомах, описывающих предметную область, в данном случае - модель памяти.
Hurd весьма громоздкое устаревшое микроядро. Я не знаю, как это у Касперского решено, но есть классические решения в Нейтрино (микроядро QNX) и в L4. Основная идея в том, чтобы сделать быстрые легковесные канады для IPC через домены общей памяти.
Спасибо, что поделились опытом и обратили внимание на некоторые аспекты языкостроительства.
Но возникает вопрос: а почему не Лисп? Там вообще ничего не нужно помнить. Ощущение, которое я испытал, написав на нём первую программу, сложнее `a + b`, было примерно такое: "Ух, ты! Да у меня процентов 50 рабочей памяти освободилось от особенностей языка под работу с самими алгоритмами!". Перешёл я на Лисп после смеси из Bash и C++. Это было физическое ощущение облегчения. У лиспов, конечно, есть свои недостатки, но это самый лёгкий для мозга язык из испробованных мной.
Если решите попробовать какой-нибудь Лисп (Scheme наиболее компактный из них, используется и в игровой индустрии), хотелось бы узнать о Вашеи опыте.
Для меня является необъяснимой загадкой каким образом не понимая подобных вещей достигли описанных в вашем профиле вершин в карьерной лестнице. Это просто невообразимо!!!
Да, в общем-то, всё просто: я всего лишь внимательно читаю документацию:
А что, люди разучились обобщать свой опыт и передавать его в более сжатой форме? Если Эйнштей 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 существуют.
Цифровые нейронные сети очень далеки от реальной архитектуры нейрона. Возможно, чтобы проявлять феномен сознания эта архитектура и не нужна, кто знает? Но реальный нейрон гораздо более сложная штука, чем то, что есть в нейросетях. Более того, реальный нейрон - это физический процесс, с квантовыми эффектами, а не просто арифметическая машина, коим является нейрон цифровой.
Вставлю свои 5 копеек. 2 цента - это если нужно развлечь публику на Хабре. Если же нужен какой-то production, то нужно учесть время, необходимое для разбора того, что сеть нагенерирует. А ошибки там бывают весьма тонкие.
Даже если мы говорим о разработке кода, когда можно всё обмазать тестами или же требованиями привести формальные доказательства корректности, где гарантии, что у сети получится это сделать за конечное время? Особенно в нетиповых ситуациях.
Я так и не смог, например, уболтать Stable Diffusion сгенерировать мне "коней, обсуждающих сферических учёных в вакууме". Думаю, любой начинающий художник за десять баксов нарисовал бы мне такой скетч за полчаса.
А как Вы определите, что он "обошёл"?
Да он и без unsafe unsound, к сожалению: https://github.com/rust-lang/rust/issues/25860. Там целая коллекция...
Даже Ксавье Леруа допускает ошибки, программируя в Коке https://sf.snu.ac.kr/sepcompcert/compcertbugs/. Куда уж нам, простым смертным? Всегда можно накосячить в аксиомах, описывающих предметную область, в данном случае - модель памяти.
Hurd весьма громоздкое устаревшое микроядро. Я не знаю, как это у Касперского решено, но есть классические решения в Нейтрино (микроядро QNX) и в L4. Основная идея в том, чтобы сделать быстрые легковесные канады для IPC через домены общей памяти.
Спасибо, что поделились опытом и обратили внимание на некоторые аспекты языкостроительства.
Но возникает вопрос: а почему не Лисп? Там вообще ничего не нужно помнить. Ощущение, которое я испытал, написав на нём первую программу, сложнее `a + b`, было примерно такое: "Ух, ты! Да у меня процентов 50 рабочей памяти освободилось от особенностей языка под работу с самими алгоритмами!". Перешёл я на Лисп после смеси из Bash и C++. Это было физическое ощущение облегчения. У лиспов, конечно, есть свои недостатки, но это самый лёгкий для мозга язык из испробованных мной.
Если решите попробовать какой-нибудь Лисп (Scheme наиболее компактный из них, используется и в игровой индустрии), хотелось бы узнать о Вашеи опыте.
Да, в общем-то, всё просто: я всего лишь внимательно читаю документацию:
https://files.pine64.org/doc/ox64/PINE64_Ox64-Schematic-202221007.pdf
🤷♂️
Мы, видимо, говорим о разных платах. Я, как и в корневом коментарии этой ветки, о Pine64 Ox64: https://wiki.pine64.org/wiki/Ox64
А что, люди разучились обобщать свой опыт и передавать его в более сжатой форме? Если Эйнштей 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 существуют.