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

"Выпуск Muen 1.0, открытого микроядра для создания высоконадёжных систем"	+/–
Сообщение от opennews (?), 25-Окт-21, 22:02
После восьми лет разработки увидел свет выпуск проекта Muen 1.0, развивающего ядро разделения (Separation kernel), отсутствие ошибок в исходных текстах которого подтверждено при помощи математических методов формальной верификации надёжности. Ядро доступно для архитектуры  x86_64 и может применяться в критически важных системах, требующих повышенного уровня надёжности и гарантии отсутствия сбоев. Исходные тексты проекта написаны на языке Ада и его верифицируемом диалекте SPARK 2014. Код распространяется под лицензией GPLv3... Подробнее: https://www.opennet.ru/opennews/art.shtml?num=56033
Ответить | Правка | Cообщить модератору

Сообщения

[Сортировка по ответам | RSS]

1. Сообщение от Онаним (?), 25-Окт-21, 22:02	+13 +/–
"написаны на языке Ада" - хорошо звучит.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #4, #14, #18, #68, #125

2. Сообщение от Аноним (2), 25-Окт-21, 22:09	–1 +/–
Есть ли там watchdog, который позволял бы ребутнуть проц без потери запущенных приложений и виртуалок.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #3

3. Сообщение от Онаним (?), 25-Окт-21, 22:13	+8 +/–
Э-э-э, а какой в этом смысл? Если возникла ситуация, в которой только реакция watchdog поможет - сохранять что-то уже поздно, и небезопасно - есть риск данных лишиться.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #2 Ответы: #33, #100

4. Сообщение от Онаним (?), 25-Окт-21, 22:16	–6 +/–
А если по делу... SATA... в критически важных системах... оценил.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #1

6. Сообщение от QwertyReg (ok), 25-Окт-21, 22:32	–5 +/–
> Ядро доступно для архитектуры x86_64 То есть даже тут x86 слили в отстойник истории. А кто-то до сих пор над десктопе насилует труп, лол.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #12, #13, #19

12. Сообщение от Аноним (12), 25-Окт-21, 22:40	–4 +/–
Действительно, сейчас все бросятся  на твой растопроц А я думал уже глупее фрактала с лошадкой быть не может. Но тут появился ты.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #6

13. Сообщение от пончик (?), 25-Окт-21, 22:43	–3 +/–
И как же ты по такой фразе сделал такой вывод? Ты бы с наркотой завязал а? пока не поздно. Или уже поздно и мозг проржавел?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #6

14. Сообщение от Аноним (-), 25-Окт-21, 23:16	–21 +/–
Хоть на васике , как бы не звучало - не на си оно никому не нужно.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #1 Ответы: #15, #25

15. Сообщение от Ingdfg (?), 25-Окт-21, 23:26	+5 +/–
Даалект который математически проверяется. Как на си это сделать? Никак.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #14 Ответы: #29, #36, #43, #149

16. Сообщение от Аноним (16), 26-Окт-21, 00:32	+/–
Нужно.
Ответить | Правка | Наверх | Cообщить модератору

17. Сообщение от Аноним (17), 26-Окт-21, 00:36	–1 +/–
Годно, оно похоронит монолитный жопаэл2рый люникс.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #26

18. Сообщение от Dzen Python (ok), 26-Окт-21, 00:53	–2 +/–
Подумать только...на АДА. А почему на сверхбезопасном и самом-мамом луДшем <deleted>?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #1 Ответы: #24, #47

19. Сообщение от Dzen Python (ok), 26-Окт-21, 00:55	–2 +/–
Единственный вопрос: почему твои посты настолько жирные, что уже даже неинтересные? Зачем?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #6 Ответы: #20

20. Сообщение от Аноним (20), 26-Окт-21, 01:03	–1 +/–
Там в пору уже к доктору сходить...
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #19

22. Сообщение от Аноним (22), 26-Окт-21, 02:54	+/–
Посоветуйте хороший учебник по языку программирования Ада пожалуйста.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #40, #45, #51, #79, #126, #140

23. Сообщение от Аноним (23), 26-Окт-21, 03:13	+/–
20 часов работает еще не зависло! Вау))
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #98

24. Сообщение от Аноньимъ (ok), 26-Окт-21, 04:05	+2 +/–
Потому, что Ада куда более структурирована, детерминирована, и поддаётся верификации. К тому же за Адой стоят промышленные стандарты. Без которых, ваши заявления о надёжности вашего ПО в контексте критических задачь, ничего не стоят.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #18 Ответы: #93

25. Сообщение от Аноньимъ (ok), 26-Окт-21, 04:10	–10 +/–
Это какая-то новая стадия отрицания. Сишка это помойный язык с нездоровым синтаксисом, околонулевой семантикой, и фрагментированой инфраструктурой. На котором можно просто и быстро писать системное ПО невероятно низкого качества.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #14 Ответы: #54, #94

26. Сообщение от Аноньимъ (ok), 26-Окт-21, 04:14	+/–
> Годно, оно похоронит монолитный жопаэл2рый люникс. Не в этой жизни. Это очень узко специализированная вещь, да ещё ни на чём кроме интела не работающая.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #17

27. Сообщение от Аноним (27), 26-Окт-21, 06:11	+/–
Альтернатива Линуксу! Годно!
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #31

29. Сообщение от МарьВанна (?), 26-Окт-21, 06:17	–14 +/–
Математическая верификация не спасает от ошибок в коде. Математическая верификация - это просто игрушка академиков и профессоров. Только чистый Си.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #15

30. Сообщение от Аноним (31), 26-Окт-21, 06:25	+6 +/–
>Код распространяется под лицензией GPLv3. Не бздуноподобная пермиссивка-разрешиловка. Зачёт.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #39, #50, #139

31. Сообщение от Аноним (31), 26-Окт-21, 06:26	+/–
>В образах компонентов с Linux задействовано ядро Linux 5.4.66. Муэн - микроядро. А Линукс- это и ещё сброник аппаратных и виртуальных драйверов.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #27 Ответы: #32

32. Сообщение от Аноним (32), 26-Окт-21, 07:02	–2 +/–
Муэн - заявочка на ядро здорового человека. Линукс - клиническая помойка.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #31 Ответы: #56, #87

33. Сообщение от Аноним (33), 26-Окт-21, 07:04	–1 +/–
смысл зависит от реализации. Вызов вачдога может запустить полную проверку контекстов. Получим надежность в целом с минимальными потерями. По крайней мере в контроллерах это прокатывает, хотя в ос конечно сложней.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #3 Ответы: #35, #92, #110

35. Сообщение от Онаним (?), 26-Окт-21, 07:29	+3 +/–
Единственный смысл - снять дамп/бектрейс (опционально) и перезапуститься. Никакая "полная проверка контекстов" не выявит причин вставания системы раком. Либо будет сложнее и затратнее самой системы. А если потенциальные причины известны и есть ресурсы на создание "проверки контекстов" - проще вложить их собственно в устранение этих причин.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #33

36. Сообщение от Онаним (?), 26-Окт-21, 07:31	+3 +/–
"Математическая верификация" гарантирует только, что оно не слетит в UB или runtime error. От разрушительного поведения в силу логических ошибок она не спасает.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #15 Ответы: #37, #80

37. Сообщение от Аноним (37), 26-Окт-21, 07:37	+2 +/–
Вам этого мало?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #36 Ответы: #57

39. Сообщение от . (?), 26-Окт-21, 08:20	–2 +/–
Ненужная ос на ненужном языке - с ненужной лицензией, все правильно. Кто-то защитил свой phd, и можно выносить.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #30 Ответы: #59

40. Сообщение от Аноним (40), 26-Окт-21, 08:22	+/–
У меня книга где то валяется так и называется "Язык Ада" , могу дать
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #22

42. Сообщение от . (?), 26-Окт-21, 08:23	–1 +/–
> Система непрерывной интеграции переведена с эмулятора Bochs на вложенные окружения QEMU/KVM. все что нужно знать об этой бесполезной поделке.
Ответить | Правка | Наверх | Cообщить модератору

43. Сообщение от Совершенно другой аноним (?), 26-Окт-21, 08:23	–1 +/–
Например так - https://www.opennet.ru/opennews/art.shtml?num=40297
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #15

44. Сообщение от Аноним (44), 26-Окт-21, 08:27	–1 +/–
А какой футпринт? Неyжто Qubes здорового человека?
Ответить | Правка | Наверх | Cообщить модератору

45. Сообщение от anonymous (??), 26-Окт-21, 08:38	+1 +/–
Была очень хорошая книжка издательства Мир (1988): Н.Джехани - Язык Ада
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #22 Ответы: #61, #72, #90

47. Сообщение от Аноним (47), 26-Окт-21, 08:57	–1 +/–
> Подумать только...на АДА. А почему на сверхбезопасном и самом-мамом луДшем <deleted>? Наверное критически поразмыслить тебе не позволяет твой жмущий сишный гениальный "мосх", да? Наверное дело _частично_ хотя бы во фразе "После восьми лет разработки увидел свет выпуск проекта Muen 1.0" (а в оригинале даже больше 8 лет - "More than eight years of continued development after the initial publication")? Ну т.е. твой объект ненависти за год то этого был еще в пеленках и непонятно чем - "Первая официальная альфа-версия Rust (0.1) была выпущена в январе 2012 года". А ада при этом с 1980-х развивалась и изначально создавалась как язык для надежного отказоустойчивого управления в реальном времени военными системами и к 2010-ым была вроде как сформировавшимся вызревшим и обкатанным стандартизованным решением?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #18 Ответы: #99

50. Сообщение от Минона (ok), 26-Окт-21, 09:13	–1 +/–
* открыл попкорн и приготовился к очередному срачу.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #30 Ответы: #95, #138

51. Сообщение от Минона (ok), 26-Окт-21, 09:19	+/–
путеводитель по Аду? Пожалуйста "https://ru.wikipedia.org/wiki/Божественная_комедия#Концепция_Ада_в_«Божественной_комедии»"
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #22 Ответы: #58

52. Сообщение от Аноним12345 (?), 26-Окт-21, 09:25	+1 +/–
Прибито гвоздями к интелу ?
Ответить | Правка | Наверх | Cообщить модератору

54. Сообщение от sdfgjsdfjdj (?), 26-Окт-21, 09:39	+2 +/–
Си - это ассемблер для ленивых. он легко позволяет делать реализации всяких resource-critical вещей, вплоть до того, что можно предсказать сколько тактов процессора займёт исполнение кода, за это его и любят
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #25 Ответы: #65, #84, #107

56. Сообщение от sdfgjsdfjdj (?), 26-Окт-21, 09:42	+/–
когда muen обрастёт таким-же количеством поддерживаемого железа - станет тоже похожа на помойку :)
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #32 Ответы: #62

57. Сообщение от Онаним (?), 26-Окт-21, 09:48	+/–
А смысл? Оно всё равно всё так же при неудачном раскладе звёзд может например потерей данных кончиться, просто в другом месте.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #37

58. Сообщение от Онаним (?), 26-Окт-21, 09:48	+/–
Да, тоже хотел Данте предложить.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #51

59. Сообщение от Онаним (?), 26-Окт-21, 09:49	+1 +/–
Ну почему ненужная-то. Да, академическая поделка. Но с учётом проделанной работы по верификации секущихся концов (не алгоритмической конечно...), вполне себе годно, только не знаю, для чего.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #39 Ответы: #69, #70

60. Сообщение от Аноним (60), 26-Окт-21, 10:08	+/–
А есть сравнение с se4L ?
Ответить | Правка | Наверх | Cообщить модератору

61. Сообщение от pofigist (?), 26-Окт-21, 10:09	+4 +/–
Да-да-да! Коричневая обложка... Еду как-то на 22м троллейбусе мимо елоховки - тогда в этом поповнике весь цвет РПЦ отирался... Читаю эту книжку... А рядом - куча воцерквленных бабок... Представляете какой цирк с конями начался, когда я книжку закрыл и они прочитали ее название? 🤣
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #45 Ответы: #91, #96

62. Сообщение от pofigist (?), 26-Окт-21, 10:11	–1 +/–
Не станет. Потому что в микроядерной архитектуре не придется все это васянское г-но тащить в ведро...
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #56 Ответы: #66

64. Сообщение от Аноним (64), 26-Окт-21, 10:37	+/–
А что там с AMD-V? Незаслуженно обидели красных.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #101

65. Сообщение от Админ Анонимов (?), 26-Окт-21, 10:41	–3 +/–
кто любит ? терпят, да, но любить ...
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #54 Ответы: #67

66. Сообщение от sdfgjsdfjdj (?), 26-Окт-21, 10:45	+/–
хех, и получишь что-то вроде 3.11 венды: микроядро, но все дрова надо качать руками (если сетка поднимется)
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #62 Ответы: #81

67. Сообщение от sdfgjsdfjdj (?), 26-Окт-21, 10:47	–1 +/–
весь HPC на сях и фортране, вряд-ли это было бы так если б язык не нравился
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #65 Ответы: #77, #109

68. Сообщение от Аноним (68), 26-Окт-21, 10:48	+2 +/–
Оно не на ADA написано, а на верифицируемом подмножестве языка ADA, диалекте ADA - языке SPARK-2014: https://en.m.wikipedia.org/wiki/SPARK_(programming_language) «The SPARK language consists of a well-defined subset of the Ada language that uses contracts to describe the specification of components in a form that is suitable for both static and dynamic verification.» https://www.adacore.com/about-spark "SPARK is a software development technology specifically designed for engineering high-reliability applications. It consists of a programming language, a verification toolset and a design method which, taken together, ensure that ultra-low defect software can be deployed in application domains where high-reliability must be assured, for example where safety and security are key requirements."
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #1

69. Сообщение от пох. (?), 26-Окт-21, 11:00	–2 +/–
Ну вот это и есть синоним ненужного - "годно не знаю для чего". Поскольку запустить из реально существующего можно только кастрированный линукс, а зачем нам еще один?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #59 Ответы: #71

70. Сообщение от Аноним (68), 26-Окт-21, 11:03	+/–
Люди на Muen OS давно девайсы выпускают, например такой: https://www.nitrokey.com/products/nethsm Меня повеселила одна фича: "наш девайсы с OS настолько безопасны, что даже консоль для ввода и вывод на монитор не предусмотрены..." Гениально! Зачем компу клава и монитор? Еще и админа тогда надо чтоб сидел и стучал по клаве, смотрел в монитор. Комп должен просто работать, без человека, как лампочка, включил и оно работает.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #59 Ответы: #76, #116

71. Сообщение от Аноним (68), 26-Окт-21, 11:08	–1 +/–
А тем временем, на SPARK-2014, под Muen OS, люди в Европе потихоньку переписывают код с C и Rust.. Решения есть, где нужна высокий уровень безопасности, стабильности и работы в режиме реального времени.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #69 Ответы: #86

72. Сообщение от доброжелатель (?), 26-Окт-21, 11:15	+/–
спасибо
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #45

76. Сообщение от Онаним (?), 26-Окт-21, 11:29	+1 +/–
А если ещё входа под кабель питания нет - вообще экстра-безопасно выйдет.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #70 Ответы: #78

77. Сообщение от Админ Анонимов (?), 26-Окт-21, 11:40	–1 +/–
тут скорее другое - жена страшная как война но держат дети
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #67 Ответы: #82

78. Сообщение от Аноним (78), 26-Окт-21, 11:41	+/–
Нет, вход для питания и выход в сеть девайсу нужны. А клавы, мониторы, даже светодиодная индикация не надо.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #76 Ответы: #102

79. Сообщение от Аноним (79), 26-Окт-21, 11:54	+1 +/–
Например, вот, от компании AdaCore: https://learn.adacore.com/ Есть ещё "А.Гавва "Адское программирование", если хотите на русском: https://www.ada-ru.org/V-0.4w/
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #22 Ответы: #111

80. Сообщение от Ingdfg (?), 26-Окт-21, 12:10	+3 +/–
По крайней мере она от чего-то спасает. А с си как? Никак.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #36 Ответы: #83

81. Сообщение от pofigist (?), 26-Окт-21, 12:11	–1 +/–
Нда... у 3.11 - микроядро... учи матчасть! Лучше как у линакса - когда в процессе установки надо качать все окружение... если сеть подымется. netinstall ога :)
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #66 Ответы: #89

82. Сообщение от sdfgjsdfjdj (?), 26-Окт-21, 12:15	–2 +/–
ты шутишь? в этих системах транспорты точат так, что за каждый лишний бранч на fast path глотку перегрызают, переменные в структурах группируют таким образом, чтобы они на одной кеш-линии оказались, да и много всего такого делают чтобы наносекунды сэкономить. вот какой ещё язык программирования такое позволяет из коробки?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #77 Ответы: #104

83. Сообщение от Совершенно другой аноним (?), 26-Окт-21, 12:34	–1 +/–
см сообщения #43 - для SeL4, который на C тоже делали "Математическую верификацию". И по-моему там тоже использовалось подмножество языка C, но его никто не называл красивыми словами SPARK-2014 или как-то ещё.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #80 Ответы: #88

84. Сообщение от Аноним (-), 26-Окт-21, 12:36	+/–
> вплоть до того, что можно предсказать сколько тактов процессора > займёт исполнение кода, за это его и любят Скорее - вплоть до самых разных баек о том, "как можно суперкруто".
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #54

85. Сообщение от uis (ok), 26-Окт-21, 12:39	–1 +/–
Ада - это Ада, это не раст. Вот где настоящая надёжность.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #103

86. Сообщение от uis (ok), 26-Окт-21, 12:41	–1 +/–
Ну вот с РВ не согласен, там лучше подходит си, а остальное - да, Ада
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #71

87. Сообщение от uis (ok), 26-Окт-21, 12:45	+/–
Угу. И количество переключений контекста тоже здоровенного человека. Особенно это весело с использованием приёмчиков предотвращения утечек по сторонним каналам.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #32

88. Сообщение от Аноним (-), 26-Окт-21, 12:46	+3 +/–
> см сообщения #43 - для SeL4, который на C тоже делали "Математическую > верификацию". И по-моему там тоже использовалось подмножество языка C, Писали на самом деле на хаскеле, лишь после верификации корректности логики работы транслируя в сишку. И обошлась та верификация где-то в 20 человеко-лет на 9000 строк кода. А так да, все с Великой Сишкой хорошо и все придумки нового - от лукавого!
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #83 Ответы: #97

89. Сообщение от sdfgjsdfjdj (?), 26-Окт-21, 12:47	–1 +/–
нда... вот и выросло поколение ЕГЭ... WinNT до версии 4.0 имела архитектуру очень сильно похожую на микроядро: большинство служб было вынесено в отдельные процессы, даже крах видеодрайвера не заваливал всю систему (да, мля, там была консоль, настоящая, как в линухе... не застал те времена?) да и вообще чтобы завалить венду NT 3.x нужно было постараться - пока консоль была доступна систему можно было вернуть к жизни без перезагрузки - наследие полуоси
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #81 Ответы: #118

90. Сообщение от uis (ok), 26-Окт-21, 12:47	+1 +/–
У Джехани вроде и по сям была книга неплохая.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #45 Ответы: #114

91. Сообщение от uis (ok), 26-Окт-21, 12:48	+1 +/–
Главное чтобы они не были вооружены тележками
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #61

92. Сообщение от uis (ok), 26-Окт-21, 12:53	+/–
> Вызов вачдога может запустить полную проверку контекстов. Если это он, то не может. Он должен делать аппаратный сброс.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #33

93. Сообщение от uis (ok), 26-Окт-21, 12:54	+/–
Мне кажется, это был сарказм
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #24 Ответы: #112

94. Сообщение от uis (ok), 26-Окт-21, 12:59	–2 +/–
> На котором можно просто и быстро писать системное ПО невероятно низкого качества. При чём тут питон? А, тьфу, питон про прикладное ПО невероятно низкого качества. Может тебе ещё и в асме синтаксис нужен? А какой, at&t или intel? Или лучше ради единственно-верного карго-культа собирать компилятор на десяток-другой гигов места под объектники и восемь гигов исходников?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #25 Ответы: #108

95. Сообщение от Аноним (-), 26-Окт-21, 13:23	+/–
Зря достал попкорн, кина не будет.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #50

96. Сообщение от Аноним (-), 26-Окт-21, 13:27	+1 +/–
Шигорину язык программирования Ада не понравится.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #61

97. Сообщение от Совершенно другой аноним (?), 26-Окт-21, 13:28	–4 +/–
>> см сообщения #43 - для SeL4, который на C тоже делали "Математическую >> верификацию". И по-моему там тоже использовалось подмножество языка C, > Писали на самом деле на хаскеле, лишь после верификации корректности логики работы > транслируя в сишку. И обошлась та верификация где-то в 20 человеко-лет > на 9000 строк кода. А так да, все с Великой Сишкой > хорошо и все придумки нового - от лукавого! что-то у Вас не сходится - Вы сами пишете, что верификация, которая выполнялась для Haskel-а, а уже потом был перевод на C, заняла 20 лет.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #88 Ответы: #113

98. Сообщение от Аноним (-), 26-Окт-21, 13:28	+/–
Отпишись поподробнее.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #23

99. Сообщение от YetAnotherOnanym (ok), 26-Окт-21, 13:58	–1 +/–
> твой объект ненависти за год то этого был еще в пеленках и непонятно чем Дык отож - пока сабж пилили, оно так и не стало ничем таким, что могло бы перетянуть к себе разработчиков и побудить их отказаться от Ады.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #47

100. Сообщение от YetAnotherOnanym (ok), 26-Окт-21, 14:00	+/–
> без потери запущенных приложений и виртуалок Чтобы сразу же после ребута влететь в то же самое состояние?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #3

101. Сообщение от Аноним (101), 26-Окт-21, 14:35	+/–
У программистов писавших Муэн материнки с процами от Интел.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #64

102. Сообщение от Онаним (?), 26-Окт-21, 14:41	+/–
Только выхода, входа из сети не надо? :D
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #78

103. Сообщение от Аноним (-), 26-Окт-21, 14:42	+/–
Только вот язык Ада - не модный.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #85 Ответы: #115

104. Сообщение от Админ Анонимов (?), 26-Окт-21, 14:56	+/–
для оптимизации узких мест есть ассемблер
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #82 Ответы: #129

107. Сообщение от Аноньимъ (ok), 26-Окт-21, 15:51	–1 +/–
>Си - это ассемблер для ленивых. он легко позволяет делать реализации всяких resource-critical вещей, вплоть до того, что можно предсказать сколько тактов процессора займёт исполнение кода Yes. >за это его и любят Любят его престарелые смузихлебы за то-же за что молодые любят жаваскрипт.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #54

108. Сообщение от Аноньимъ (ok), 26-Окт-21, 15:58	–1 +/–
>При чём тут питон? А, тьфу, питон про прикладное ПО невероятно низкого качества. Да, сишка это системный питон такой. Врайт ванце краш еверивере. >Может тебе ещё и в асме синтаксис нужен? В сишке синтаксиса очень очень дофига. Я никогда не говорил что в сишке не хватает синтаксиса. Речь шла о том, что он ужасный, и лишённый семантики. >А какой, at&t или intel? Или лучше ради единственно-верного карго-культа собирать компилятор на десяток-другой гигов места под объектники и восемь гигов исходников? Чё? Да, GCC ужасный монстр, я согласен. Монструозность GCC, к которому ещё и систему сборки нужно отдельно прикручивать, и систему управления пакетами, хорошо демонстрирует мною сказанное.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #94 Ответы: #127

109. Сообщение от Аноньимъ (ok), 26-Окт-21, 16:00	–2 +/–
>>кто любит сишку? терпят, да, но любить ... >весь HPC на фортране любит Хмммммммм?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #67

110. Сообщение от Аноним (33), 26-Окт-21, 16:14	+/–
да успокойтесь уже, не говорится в этой оси про вачдог. Речь была о контроллере. Была необходимость и было так сделано. Какие блин виртуалки?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #33

111. Сообщение от Аноним (22), 26-Окт-21, 16:16	+/–
Спасибо
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #79

112. Сообщение от Аноньимъ (ok), 26-Окт-21, 16:19	+/–
Ада с рустом это как мягкое с солёным. Раст это про функциональщину и безопасность памяти. Ада это структурированный объектный подход и надежность. Раст ищет компромисс между системным и прикладным программированием. Между скоростью кода, скоростью разработки, и количеством ошибок. Ада же ставит целью создание максимально детерминированных программ не делающих ничего лишнего но делающих всё нужное. Исполняемых максимально однообразно. При этом код должен быть максимально прозрачный и читаемый человеком. Поэтому Ада в принципе один из самых подходящих языков для написания ОС, любой. Только на ней и нужно писать такие вещи(можно ли другой вопрос). Раст это не особо про надежность, не фонтан(не фортран лол) в целом, но есть в нем и плюсы, я ставлю его в категорию - и так сойдёт.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #93 Ответы: #128

113. Сообщение от Аноним (-), 26-Окт-21, 16:34	+/–
> что-то у Вас не сходится - Вы сами пишете, что верификация, которая > выполнялась для Haskel-а, а уже потом был перевод на C, заняла 20 лет. У тех, кто лишь ту новость и читал, но ни по каким сылкам не ходил: http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf > The overallsize of the proof,including framework, libraries, and generated proofs (not shown in the table)is 200,000 lines of Isabelle script. > The abstract spec took about 4 person months to develop > About 2 person years (py) went into Haskell prototype ... > The initial C translation was donein 3 weeks, in total the C implementation took about 2 pm,for a total costof 2.2 py including the Haskell effort. ... > The cost of the proof is higher,in total about 20 py. и с верификацией знаком лишь из заголовка новости - все может быть.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #97

114. Сообщение от YetAnotherOnanym (ok), 26-Окт-21, 16:34	+/–
Ага, в волосатой обложке )))
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #90

115. Сообщение от Anonymous XE (?), 26-Окт-21, 16:42	+/–
Это хорошо, модно-молодёжные в него лезть не будут.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #103 Ответы: #117, #123

116. Сообщение от Anonymous XE (?), 26-Окт-21, 16:52	+/–
Действительно, зачнм независающей ОС локальная консоль? А для конфигуряния есть же SSH.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #70

117. Сообщение от Аноним (-), 26-Окт-21, 17:12	+/–
Старые программисты на Ада умрут от старости, без модной молодёжи кому вы свою Адскую Отчизну оставите? Или думаете, как в Дебиане, на вашу сторону появится поток из стареющих пацанов?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #115

118. Сообщение от pofigist (?), 26-Окт-21, 17:34	+/–
> нда... вот и выросло поколение ЕГЭ... Да уж - заметно. Нет и никогда не было WinNT 3.11 - это была Windows for Worksgroup, в которой никаким микроядром и не пахло... WinNT была либо 3.1, либо 3.50 либо 3.51... И там таки да - было микроядро. Впрочем почему было - оно и сейчас там есть... Просто не совсем классической схемы.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #89 Ответы: #130

119. Сообщение от Аноним (119), 26-Окт-21, 17:38	+/–
Кто на Аду будет вкатываться, есть такие?
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #124, #147

123. Сообщение от Anonymous XE (?), 26-Окт-21, 18:18	+/–
Молодые и модно-молодёжные, это, как бы, не эквивалентно.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #115

124. Сообщение от Аноним (-), 26-Окт-21, 18:37	+/–
многаденех курсы бисплатные личная пальма под цвет ноутбука ада за 24 часа от нуля до гираскутера  гламурная барада в пакете с первой дозой в падарок
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #119 Ответы: #133

125. Сообщение от Kuromi (ok), 26-Окт-21, 19:45	+/–
При загрузке из колонок раздается Descent Into Cerberon из Quake 2
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #1

126. Сообщение от Kuromi (ok), 26-Окт-21, 19:46	+/–
Некрономикон (под ред. Брюса "Эш" Кэмпбелла)
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #22

127. Сообщение от Онаним (?), 26-Окт-21, 19:57	+/–
> В сишке синтаксиса очень очень дофига. Я никогда не говорил что в сишке не хватает синтаксиса. > Речь шла о том, что он ужасный, и лишённый семантики. Лучше и читабельнее пока не придумано, все эти питорастические извраты так извратами и останутся. Нет, из сей тоже можно сделать троллейбус, как из той буханки, но если писать не ради извращения - будет читабельно.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #108

128. Сообщение от Онаним (?), 26-Окт-21, 19:58	+/–
Хрусту надо больше Ада.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #112

129. Сообщение от sdkhflskhgl (?), 26-Окт-21, 20:17	+/–
пробовал на асме большие проекты делать? а под несколько архитектур? да хотя бы под несколько процов одной архитектуры?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #104

130. Сообщение от sdkhflskhgl (?), 26-Окт-21, 20:19	+/–
да, затупил, не тот минор написал, давно дело было, забывать стал
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #118 Ответы: #148

131. Сообщение от Gogi (??), 26-Окт-21, 20:30	+/–
Мне от одного списка (аппаратных) возможностей плохо стало! Неужели ВСЁ ЭТО нужно для того, чтобы юзер тупо запустил ворд?? (условно говоря) По-моему, проектировщики аппаратуры стали такой же тупой индуснёй, как и в софте - главное наструячить побольше фич, а надо оно или нет - да пофиг, оплачено! (как было с x86 + защищённый режим + тонна сопутствующих НЕНУЖНЫХ регистров, таблиц и т.п.) Гениальное обязано быть простым и понятным. Если какую-то платформу раздули до неосязаемых архитектурных громад, нахрен такую архитектуру. Я лучше на БК0010 буду редактировать, чем на суперзащищённом x86 ждать, когда меня вскроют через IME.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #132, #142

132. Сообщение от Онаним (?), 26-Окт-21, 20:44	+/–
Главное - не смотри на инициализацию ACPI и PCI в линуховом ядре... Вот где ад так ад.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #131

133. Сообщение от Аноним (-), 27-Окт-21, 06:31	+/–
Райдер модного, молодёжного и прогрессивного человека. 1. Много денег. 2. Бесплатные курсы по языку Ада. 3. Свой остров, или пляж с пальмами под цвет ноутбука. 4. Книжка "Освой Ада за 24 часа". 5. Гироскутер. 6. Гламурная борода. 7. Доза веществ в пакете (в подарок). Нужно для того чтобы возникали в голове творческие мысли. В принципе всё, юридически оформил. Пунк 7 хорошо реализуем в Калифорнии, либо в Нидерландах.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #124

137. Сообщение от Аноним (138), 27-Окт-21, 10:18	+/–
Открытый и (высоко)надёжный таки разные вещи. Друг с другом никак не связанные.
Ответить | Правка | Наверх | Cообщить модератору
Ответы: #145

138. Сообщение от Аноним (138), 27-Окт-21, 10:19	+/–
А почему под срач так хорош именно попкорм? А горох не лучше?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #50 Ответы: #141, #143

139. Сообщение от Аноним (138), 27-Окт-21, 10:20	+/–
Закрытый таки всегда надёжнее. Чем распахнутый.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #30

140. Сообщение от PnD (??), 27-Окт-21, 10:41	+1 +/–
Вот тут мне нравится как концепции показывают: http://www.ada-ru.org/safe_secure_2012
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #22

141. Сообщение от Минона (ok), 27-Окт-21, 10:47	+/–
какой? зеленый из баночки? попробуй ☺
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #138

142. Сообщение от Аноним (142), 27-Окт-21, 11:40	+/–
на суперзащищенном airgap ждать пока вскроют через трансформатор
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #131

143. Сообщение от Аноним (-), 27-Окт-21, 12:00	+/–
Для того чтобы наслаждаться срачем со сороны, не учавствуя в нём, нужен мягкий диван и попкорн. Всё.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #138 Ответы: #144

144. Сообщение от Аноним (138), 27-Окт-21, 12:45	+/–
А пыво???
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #143

145. Сообщение от Аноним (142), 27-Окт-21, 12:48	+/–
сперва академическое открытое, потом уж точное наведение на нужную голову в реалтайм. но цена головы/репутации с нулевых сильно упала, потому можно и гражданским линуксом по квадрату с задержкой и осечкой.
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #137 Ответы: #146

146. Сообщение от Аноним (-), 27-Окт-21, 14:28	+/–
>гражданским линуксом по квадрату с задержкой и осечкой. Это вояка?
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #145

147. Сообщение от Аноним (33), 27-Окт-21, 17:08	+/–
Аду же разрабатывала оборонка америки. Наса на ней клепала управление своими шатлами. Помнится трапалась на пуске по каждому чиху. Но работала вроде надежно. Программисты на ней писали кажется только для ихнего впк, про гражданские проекты не слышно было
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #119

148. Сообщение от pofigist (?), 28-Окт-21, 16:58	+/–
Это деменция... Прививался чтоль? :) Такое перепутать - невозможно! :)
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #130

149. Сообщение от читатель (?), 29-Окт-21, 22:49	+/–
frama-c, погуглите
Ответить | Правка | Наверх | Cообщить модератору
Родитель: #15

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

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