forum.opennet.ru - "Проекту seL4 присуждена премия ACM Software System Award" (49)

"Проекту seL4 присуждена премия ACM Software System Award"

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

"Проекту seL4 присуждена премия ACM Software System Award"	+/–
Сообщение от opennews (??), 06-Май-23, 22:34
Проект, развивающий открытое микроядро seL4, получил премию ACM Software System Award, ежегодно присуждаемую Ассоциация вычислительной техники (ACM), наиболее авторитетной международной организации в области компьютерных систем. Премия присуждена за достижения в области математического доказательства надёжности работы, которое свидетельствует о полном соответствии заданным на формальном языке спецификациям и признаёт готовность использования в критически важных применениях. Проект seL4 показал, что можно не только полностью провести формальную верификацию надёжности и безопасности для проектов уровня промышленных операционных систем, но и добиться этого без ущерба производительности и универсальности... Подробнее: https://www.opennet.ru/opennews/art.shtml?num=59091
Ответить \| Правка \| Cообщить модератору

Оглавление

Скоро Фуксия со своим Цирконом спустится и покроет всё стадо , Аноним (1), 22:34 , 06-Май-23, (1)

Угу, спустится, с высот фоторамки и что там еще - говорящий кофейник Не хотел бы, пох. (?), 22:38 , 06-Май-23, (3) –1

Про джаву тоже говорили что он только для кофемашин И где сейчас джава Да она , Аноним (1), 23:11 , 06-Май-23, (5) +1

Ну да - на всех кладбищах enterprise environment Новых проектов на ней нет К, _ (??), 04:15 , 08-Май-23, (36)

Ксожалению, таки есть Для новых прозектов берут Швинг и продолжают пейсать на д, Аноним (38), 08:49 , 08-Май-23, (38) –1

А чем Котлин не джава , Аноним (39), 11:20 , 08-Май-23, (39) +1

Однако эти кладбища почему-то способны платить тебе стабильную хорошую ЗП, в о, Аноним (63), 21:00 , 11-Май-23, (63)

Да не везде, и вообще она давно закатывается И даже graalvm её не вытянет Как р, Заноним (?), 18:51 , 08-Май-23, (40)

Мне нравятся такие древние языки Чем меньше дешёвой школоты хочет с ней работа, Аноним (63), 21:01 , 11-Май-23, (64)

Ну на java столько понаписали, что ЗП ещё долго будут платить , Заноним (?), 00:28 , 12-Май-23, (65)

у гугла и на sel4 есть ОСhttps www opennet ru opennews art shtml num 57920, Аноним (43), 21:36 , 08-Май-23, (43) +1

Очень крутой проект, показывающий насколько тяжело и дорого так разрабатывать со, Анонн (?), 23:20 , 06-Май-23, (6) +7

Поэтому Hurd и не смогли дописать , Аноним (1), 23:29 , 06-Май-23, (7) –1

Нет, его к счастью писали, а не верифицировали-верифицировали Просто на фоне лин, пох. (?), 00:10 , 07-Май-23, (10) –2

в этом контексте для проектов уровня промышленных операционных систем звучит с, vitalif (ok), 23:32 , 06-Май-23, (8)

промышленная - это в промышленности Каким-нибудь приводом конвейера управлять, , пох. (?), 23:09 , 08-Май-23, (45)

верификацияСлово проверка ведь с более меньшим углеродным следом, товарищи , Аноним (22), 08:33 , 07-Май-23, (22) –1

Верификация - проверкаАутентификация - проверкаАвторизация - проверкаВалидация -, Аноним (41), 19:24 , 08-Май-23, (41) +5

Интересные подробности Я особенно обратил бы внимание на то, что 1 это всё пок, warlock66613 (ok), 20:58 , 08-Май-23, (42)

Скрыто модератором, InuYasha (??), 23:37 , 06-Май-23, (9) –1

Скрыто модератором, пох. (?), 00:11 , 07-Май-23, (11) +2

Скрыто модератором, Аноним (12), 01:01 , 07-Май-23, (12) –1

Скрыто модератором, Аноним (18), 03:56 , 07-Май-23, (18)
Скрыто модератором, пох. (?), 09:55 , 07-Май-23, (26) +1

Скрыто модератором, tty0 (?), 01:03 , 07-Май-23, (13)

Скрыто модератором, Прохожий (??), 02:08 , 07-Май-23, (16) –5

Скрыто модератором, пох. (?), 09:58 , 07-Май-23, (27)

Они что-то там на Haskell начудили, молодцы А я могу таким же образом мой код ве, Аноним (24), 08:54 , 07-Май-23, (24)

Нет Вы же наверняка используете сторонние библиотеки, как минимум стандартную б, warlock66613 (ok), 12:16 , 10-Май-23, (61)

шта А можно чуть подробнее, на что повлияла разработка seL4 Может, какие-то О, Аноним (29), 12:48 , 07-Май-23, (29)

https www opennet ru opennews art shtml num 59052Это Вам не подойдет , Аноним (31), 13:47 , 07-Май-23, (31) –1
Болгары восхитились Ну и вообще, чего докопался, это не троллейбус из буханки,, пох. (?), 16:34 , 07-Май-23, (32)
Проекту seL4 присуждена премия ACM Software System Award, Степан (?), 19:02 , 07-Май-23, (33)

О, точно, двадцать плетей басурманину Столешница, скоморох , пох. (?), 21:54 , 07-Май-23, (35) +1

на разработку современных систем применяемых в критически важных областях - авто, Аноним (43), 21:47 , 08-Май-23, (44) +1

чегой-то мне кажется что мэйнстрим сейчас - как в тойете с педалью газа Когда п, пох. (?), 23:17 , 08-Май-23, (46)

майнстрим сейчас исключить человеческий фактор из управления автомобилямиhttps , Аноним (43), 10:27 , 09-Май-23, (47)

Ну вот тойета опередила тренд на десять лет Правда, исключенному человеческом, пох. (?), 11:28 , 09-Май-23, (48)
Майстрим сейчас, как и всегда - подоить доверчивых лошк W инвесторов и потребляd, Аноним (49), 12:37 , 09-Май-23, (49) +1

Ну зочем вы тгавите - Маск всего двух только пока и убил Ну трех если считать , пох. (?), 15:24 , 09-Май-23, (52)
для развития технологий нужны финансы это очевидно, но вы покупаете товары потом, Аноним (43), 16:25 , 09-Май-23, (54)

А в огороде бузина, это тоже очевидно Внезапно, можно развивать технологии и при, Аноним (49), 17:16 , 09-Май-23, (55)

внезапно переход от L2 к L3 имеет чисто правовые сложности - после сертификации , Аноним (43), 23:28 , 09-Май-23, (59)

Угу, чисто правовые сложности опять танцорам мешают, а не то они бы всем показ, Аноним (49), 11:37 , 10-Май-23, (60) +1

сказки не надо рассказывать - когда там всплеск развития ИИ начался несколько , Аноним (43), 09:31 , 11-Май-23, (62) –1

с моей точки зрения вся эта идея формальной верификации микроядра и полученной з, Аноним (51), 14:04 , 09-Май-23, (51) –2

поток сознания эксперта опеннетаПро то что такое формальная верификация и как эт, пох. (?), 15:26 , 09-Май-23, (53) +1

Строгое математическое доказательство показало, что все предусмотренные ТЗ бекдо, fidoman (ok), 19:45 , 07-Май-23, (34) –2
лично мне чужды подобные инновационные решения встроеных систем, я предпочитаю р, Аноним (51), 14:03 , 09-Май-23, (50) –4

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

1. Сообщение от Аноним (1), 06-Май-23, 22:34 +/–

Скоро Фуксия со своим Цирконом спустится и покроет всё стадо.

Ответить | Правка | Наверх | Cообщить модератору
Ответы: #3, #43

3. Сообщение от пох. (?), 06-Май-23, 22:38 –1 +/–

Угу, спустится, с высот фоторамки и что там еще - говорящий кофейник?
Не хотел бы тебя огорчать, дружище, но это дно. С него спускаться дальше некуда. Сдохла твоя фикция, не взлетела.
В принципе, конечно, от sel4 тоже толку никакого, занятный но феерично ненужный артефакт.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #1 Ответы: #5

5. Сообщение от Аноним (1), 06-Май-23, 23:11 +1 +/–

Про джаву тоже говорили что он только для кофемашин. И где сейчас джава? Да она везде, бро!

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #3 Ответы: #36, #40

6. Сообщение от Анонн (?), 06-Май-23, 23:20 +7 +/–

Очень крутой проект, показывающий насколько тяжело и дорого так разрабатывать софт.
Там всего меньше 10к строк кода ("8,700 lines of C code and 600 lines of assemble" если быть точным).
При этом "затраты" на аналогичную верификацию при уже проработанной методологии - 8 (восемь) человеко-лет ("kernel plus proof of 8 py")
В процессе верификации пришлось писать кучу уточнений,
нашли 16 дефектов до второй фазы верификации, сама формальная верификация нашла 144 дефекта и необходимость внести 54 изменения. Т.е. где-то 1 дефект на 50 строк си/асм кода.
Подробности тут: https://www.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf

Ответить | Правка | Наверх | Cообщить модератору
Ответы: #7, #8, #22, #42

7. Сообщение от Аноним (1), 06-Май-23, 23:29 –1 +/–

Поэтому Hurd и не смогли дописать.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #6 Ответы: #10

8. Сообщение от vitalif (ok), 06-Май-23, 23:32 +/–

в этом контексте "для проектов уровня промышленных операционных систем" звучит слегка забавно

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #6 Ответы: #45

9. Сообщение от InuYasha (??), 06-Май-23, 23:37 –1 +/–

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

Ответить | Правка | Наверх | Cообщить модератору
Ответы: #11, #16

10. Сообщение от пох. (?), 07-Май-23, 00:10 –2 +/–

Нет, его к счастью писали, а не верифицировали-верифицировали.
Просто на фоне линукса это неповоротливое чудовище (с драйверами, как нельзя более кстати, копипащенными из линукса же) оказалось никому совершенно не нужным.
Т.е. добились что оно загружалось и можно было даже набрать /bin/ls - но что делать дальше все равно никто не знал.
А это недоразумение даже и такого не может.

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

11. Сообщение от пох. (?), 07-Май-23, 00:11 +2 +/–

Ну если честно - их ресдох хотя бы был похож на законченую операционную систему. А тут голое микроядро непонятно для чего, зато верифицированное.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #9 Ответы: #12, #13

12. Сообщение от Аноним (12), 07-Май-23, 01:01 –1 +/–

Почему "непонятно для чего"?
Как раз понятно - чтобы использовать его как запускалку виртуальных машин и быть уверенным что не выйдет за пределы виртуалки.
"seL4 can run Linux in a virtual machine. seL4 is [...] hypervisor with a sound worst-case execution-time (WCET) analysis, and as such the only one that can give you actual real-time guarantees, no matter what others may be claiming."

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #11 Ответы: #18, #26

13. Сообщение от tty0 (?), 07-Май-23, 01:03 +/–

Проблема в том, что людей, которым нужен не продукт, а инструмент слишком мало. На этом проекте можно реализовать очень крутые вещи, к примеру, захардкодив ядро целиком в железе. Но это слишком долго, а значит будем по старинке - нестабильное ядро и много обновлений

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

16. Сообщение от Прохожий (??), 07-Май-23, 02:08 –5 +/–

С логикой и здравым смыслом у очередного местного аналитика (от слова анал) всё, как обычно, то есть никак.
Если уж кто и будет задыхаться и дёргаться в припадках, так это Сишники. 9 тыс. строк кода и 8 лет верификации - прекрасная производительность (нет). Не говоря уж о стоимости.
Куда лучше всё-таки, когда от подавляющей части ошибок защищает компилятор прямо во время разработки. Остальные верифицировать займёт куда меньше времени.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #9 Ответы: #27

18. Сообщение от Аноним (18), 07-Май-23, 03:56 +/–

Осталось ешё верифицированную виртулку написать. Если неверифицированную, то можно Genode взять.

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

22. Сообщение от Аноним (22), 07-Май-23, 08:33 –1 +/–

верификация
Слово "проверка" ведь с более меньшим углеродным следом, товарищи.. )

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #6 Ответы: #41

24. Сообщение от Аноним (24), 07-Май-23, 08:54 +/–

Они что-то там на Haskell начудили, молодцы.
А я могу таким же образом мой код верифицировать?
У меня есть несколько крошечных проектов, на тысячу строк.

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

26. Сообщение от пох. (?), 07-Май-23, 09:55 +1 +/–

> Почему "непонятно для чего"?
> Как раз понятно - чтобы использовать его как запускалку виртуальных машин и
для запускалки виртуальных машин общего назначения а не чего-то совсем не от мира сего - надо уметь в сети, диски, межхостовый обмен, паравиртуализацию и Б-г знает чего еще кажущееся очевидным я забыл.
А тут ничего нет, пустыня.
> быть уверенным что не выйдет за пределы виртуалки.
виртуалка без сети, дисков и управления и так никуда не выйдет, а выйдет так пожалеет что вышла - потому что там опять ничегошеньки нет.
То есть написать это все (неизвестно, между нами, с какой итоговой производительносью и куда при этом пойдет верифицированность) наверное можно, но нереально - нет у человечества столько лишних кодеров.
Остаются только совсем уж странные нишевые применения, а поскольку те никогда не будут массовыми - рынок и в этих нишах выберет что попроще и попонятнее.

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

27. Сообщение от пох. (?), 07-Май-23, 09:58 +/–

> Куда лучше всё-таки, когда от подавляющей части ошибок защищает компилятор прямо во
> время разработки. Остальные верифицировать займёт куда меньше времени.
да, просто прекрасно. Все время разработки уходит на борьбу с компилятором, потом чувак сдается и пишет unsafe {мамойклянус!}
Результат - компилятор успешно защитил, нет разработки нет и ошибок.
Не правда ли, ресдох?

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

29. Сообщение от Аноним (29), 07-Май-23, 12:48 +/–

> вручается за разработку программных систем, оказавших определяющее влияние на отрасль
шта?! А можно чуть подробнее, на что повлияла разработка seL4? Может, какие-то ОС на ней написали годные? Хотя бы уровня Линукса - 1% декстопа и то хорошо. Или seL4 только тем и хороша, что про неё ГОДАМИ только и можно писать, что она "верифицируемая"? :))))))) (проверяемая, клоуны!)

Ответить | Правка | Наверх | Cообщить модератору
Ответы: #31, #32, #33, #44

31. Сообщение от Аноним (31), 07-Май-23, 13:47 –1 +/–

https://www.opennet.ru/opennews/art.shtml?num=59052
Это Вам не подойдет?

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

32. Сообщение от пох. (?), 07-Май-23, 16:34 +/–

> А можно чуть подробнее, на что повлияла разработка seL4?
"Болгары восхитились!"
Ну и вообще, чего докопался, это не троллейбус из буханки, это корабль в бутылке в форме буханки. Кросивое! Поставить в музей на центральное место экспозиции, ходить вокруг на цыпочках, умиляться. Потом, когда-нибудь, обнаружим что интел впилил ее в ядро своего ME заместо нынешнего (тоже троллейбуса но гораздо менее выдающегося) или еще где в подобном месте всплывет.
> (проверяемая, клоуны!)
этому - десять плетей за иноземные слова воспрещенные.
Не клоуны, а скоморохи!
Клоуны - это когда в DF докопался до адамантина на один лишний кубик.

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

33. Сообщение от Степан (?), 07-Май-23, 19:02 +/–

> декстопа
> проверяемая, клоуны

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #29 Ответы: #35

34. Сообщение от fidoman (ok), 07-Май-23, 19:45 –2 +/–

Строгое математическое доказательство показало, что все предусмотренные ТЗ бекдоры на месте.

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

35. Сообщение от пох. (?), 07-Май-23, 21:54 +1 +/–

О, точно, двадцать плетей басурманину! Столешница, скоморох!

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

36. Сообщение от _ (??), 08-Май-23, 04:15 +/–

Ну да - на всех кладбищах (enterprise environment). Новых проектов на ней нет. Как и предсказывалось - новый Кобол :(

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #5 Ответы: #38, #63

38. Сообщение от Аноним (38), 08-Май-23, 08:49 –1 +/–

Ксожалению, таки есть. Для новых прозектов берут Швинг и продолжают пейсать на джяве. И логика в этом есть, и есть причины так делать.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #36 Ответы: #39

39. Сообщение от Аноним (39), 08-Май-23, 11:20 +1 +/–

А чем Котлин не джава?

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

40. Сообщение от Заноним (?), 08-Май-23, 18:51 +/–

Да не везде, и вообще она давно закатывается. И даже graalvm её не вытянет.
Как ранее сказали - очередной cobol.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #5 Ответы: #64

41. Сообщение от Аноним (41), 08-Май-23, 19:24 +5 +/–

Верификация - проверка
Аутентификация - проверка
Авторизация - проверка
Валидация - проверка

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

42. Сообщение от warlock66613 (ok), 08-Май-23, 20:58 +/–

Интересные подробности. Я особенно обратил бы внимание на то, что 1) это всё пока без поддержки многоядерности/мультипроцессорности, 2) им пришлось жёстко отказаться от указателей на стек: если в коде указатель, то его цель — в куче. Довольно серьёзные ограничения, особенно если подумать о них вместе.

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

43. Сообщение от Аноним (43), 08-Май-23, 21:36 +1 +/–

> Скоро Фуксия
у гугла и на sel4 есть ОС
https://www.opennet.ru/opennews/art.shtml?num=57920

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

44. Сообщение от Аноним (43), 08-Май-23, 21:47 +1 +/–

> на что повлияла разработка seL4?
на разработку современных систем применяемых в критически важных областях - автомобильной, медицинской, аерокосмической, военной. Сейчас майнстрим - гипервизор на клонах L4, см например
https://en.wikipedia.org/wiki/PikeOS

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #29 Ответы: #46

45. Сообщение от пох. (?), 08-Май-23, 23:09 +/–

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

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

46. Сообщение от пох. (?), 08-Май-23, 23:17 +/–

чегой-то мне кажется что мэйнстрим сейчас - как в тойете с педалью газа. Когда при наличии двухканального датчика индус ляпает еще один китайский глючный (потому что не знает про второй канал или не умеет вообще в тот датчик) а потом кодит такое что счастливый клиент убивается апстену. Всем похрену.
https://en.wikipedia.org/wiki/PikeOS
It enables users to build certifiable smart devices for the Internet of things (IoT)
Т.е. и этим прекрасным микроскопом просто забивают гвозди.
Ну в общем логично, учитывая eclipse и прочий трэшачок.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #44 Ответы: #47, #51

47. Сообщение от Аноним (43), 09-Май-23, 10:27 +/–

> мне кажется что мэйнстрим сейчас - как в тойете с педалью газа
майнстрим сейчас исключить человеческий фактор из управления автомобилями
https://www.mobileye.com/
> Т.е. и этим прекрасным микроскопом просто забивают гвозди
они зарабатывают на всём, денег больше всего в ширпотребе. В автомобилях выпускаемых в Германии используют открытый фреймворк l4re
https://www.kernkonzept.com

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #46 Ответы: #48, #49

48. Сообщение от пох. (?), 09-Май-23, 11:28 +/–

Ну вот тойета опередила тренд на десять лет. Правда, "исключенному" человеческому фактору кажется не очень понравилось вляпываться в стену.

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

49. Сообщение от Аноним (49), 09-Май-23, 12:37 +1 +/–

> майнстрим сейчас исключить человеческий фактор из управления автомобилями
> https://www.mobileye.com/
Майстрим сейчас, как и всегда - подоить доверчивых лошк^W инвесторов и потребляd^Hтелей.
Маск вон, уже почти десять лет - "еще немного и уже почти совсем скоро" и ниче, пипл хавает за обе щеки.
А в реальности, хорошо если лет через 15-20 что-то не сильно стремное в этой области появится.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #47 Ответы: #52, #54

50. Сообщение от Аноним (51), 09-Май-23, 14:03 –4 +/–

лично мне чужды подобные инновационные решения встроеных систем, я предпочитаю разрабатывать прикладные решения на языке си-плюсплюс в среде майкрософт визуал студио, а для моих задач со средней нагрузкой предпочтительнее простой монолитный ядренной архитектуры виндовс,которая проверенная временем и хорошо изученная, а эти "легковесные" микроядра только усложняют работу без очевидных преимуществ для обычного прикладного разработчика,как говорится "если не сломалось - не чини" и кто то явно преувеличивает значимость этого проекта чтобы получить гранты и деньги, поэтому я не вижу ничего выдающегося в этом проекте и его награждении

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

51. Сообщение от Аноним (51), 09-Май-23, 14:04 –2 +/–

с моей точки зрения вся эта идея формальной верификации микроядра и полученной за это награды преувеличена и не имеет реальной ценности.
во-первых для большинства реальных задач разработчикам подобные фокусы с "абстрактной точностью" не нужны, нам надо производительные и стабильные решения, а не надменные громоздкие конструкции инженеров.
во-вторых я не верю что полная формальная верификация реально возможна, в любой сложной системе остаются упущения и баги которые обнаружатся только во время работы.
в-третьих похоже что весь этот проект продвигается ради грантов и личного признания его создателей, несмотря на отсутствие какой-либо реальной пользы для большинства пользователей. пиар и завышенные ожидания - основные инструменты для привлечения средств.
поэтому лично я считаю что эта награда не оправдана и проект не решает реальные проблемы, скорее это очередное "блестящее" теоретическое предложение без настоящей ценности, а награда лишь демонстрирует избирательность экспертов.
в целом мне кажется что много шума из ничего, типичная "технологическая хайпа" с целью получения финансирования и продвижения, а не ради каких-то реальных достижений или прорывов

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #46 Ответы: #53

52. Сообщение от пох. (?), 09-Май-23, 15:24 +/–

Ну зочем вы тгавите - Маск всего двух только пока и убил. (Ну трех если считать отправленного в космос с билетом в один конец)

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

53. Сообщение от пох. (?), 09-Май-23, 15:26 +1 +/–

поток сознания эксперта опеннета
Про то что такое формальная верификация и как это работает - читать ему разумеется, не интересно и незачем, у него уже есть ценное мнение.

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

54. Сообщение от Аноним (43), 09-Май-23, 16:25 +/–

> Майстрим сейчас, как и всегда - подоить доверчивых лошк^W инвесторов и потребляd^Hтелей.
для развития технологий нужны финансы это очевидно, но вы покупаете товары потому что лош.к ? а я думаю что для собственного комфорта. Но конечно можете и на собачках скакать вместо автомобилей. И ж..у берестой подтирать, бумага для лошк.в

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #49 Ответы: #55

55. Сообщение от Аноним (49), 09-Май-23, 17:16 +/–

>> Майстрим сейчас, как и всегда - подоить доверчивых лошк^W инвесторов и потребляd^Hтелей.
> для развития технологий нужны финансы это очевидно, но вы покупаете товары потому что лош.к ?
А в огороде бузина, это тоже очевидно.
Внезапно, можно развивать технологии и при этом выдавать продвинутых ассистентов в качестве промежуточного результата - _уже__работающих_, хоть и с определенными ограничениями, как например мерседес с их ассистентом, прошедшим SAE-Level-3 сертификацию.
А можно почти 10 лет просто обещать "уже почти совсем готово еще чуть-чуть!".

> а я думаю что для собственного комфорта. Но конечно можете и на собачках скакать вместо автомобилей. И ж..у берестой подтирать, бумага для лошк.в
"Как вместо ответа по существу или хотя бы по теме, создать абстрактное соломенное чучело и победить его, Опеннетная Демонстрация №100501"

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #54 Ответы: #59

59. Сообщение от Аноним (43), 09-Май-23, 23:28 +/–

> Внезапно, можно развивать технологии и при этом выдавать продвинутых ассистентов в качестве промежуточного результата - _уже__работающих_, хоть и с определенными ограничениями, как например мерседес с их ассистентом, прошедшим SAE-Level-3 сертификацию.
внезапно переход от L2 к L3 имеет чисто правовые сложности - после сертификации L3 производитель берёт на себя отвественность при аварии по вине автопилота, а мерседесы сертифицирован только в Германии и штате Невада
https://autocrypt.io/the-state-of-level-3-autonomous-driving.../
технически возможен L5 уже сейчас, см YeyQ Ultra
https://www.mobileye.com/technology/eyeq-chip
а ваши "в реальности, хорошо если лет через 15-20 что-то не сильно стремное в этой области появится" это просто газификация луж

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #55 Ответы: #60

60. Сообщение от Аноним (49), 10-Май-23, 11:37 +1 +/–

> внезапно переход от L2 к L3 имеет чисто правовые сложности - после сертификации L3 производитель берёт на себя отвественность при аварии по вине автопилота, а мерседесы сертифицирован только в Германии и штате Невада
Угу, "чисто правовые сложности" опять танцорам мешают, а не то они бы всем показали.
Внезапно, это и есть тот самый "нюанс, Петька" - когда производитель берет ответственность за свои заявления, а не прячет мелким шрифтом "работающий супер-автопилот-аналогов-нет ... только будьте готовы в любой момент перехватить управления и если что, мы не виноваты, виноваты вы!".

> https://autocrypt.io/the-state-of-level-3-autonomous-driving.../
> технически возможен L5 уже сейчас, см YeyQ Ultra
Он "возможен" уже хрен его знает сколько лет - но только "на свой страх и риск". Т.е. то самое пресловутое "прорыв уже-почти-еще-немного".
> а ваши "в реальности, хорошо если лет через 15-20 что-то не сильно стремное в этой области появится" это просто газификация луж
Ну давай ссылку, где приобрести такую бибику, раз газификатор тут не ты. Только учти - "не сильно стремное" предполагает как раз, что произовдитель не только умеет в красивый маркетинг и обещания, но и еще и отвечать за свои слова.

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #59 Ответы: #62

61. Сообщение от warlock66613 (ok), 10-Май-23, 12:16 +/–

Нет. Вы же наверняка используете сторонние библиотеки, как минимум стандартную библиотеку.

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

62. Сообщение от Аноним (43), 11-Май-23, 09:31 –1 +/–

> Он "возможен" уже хрен его знает сколько лет - но только "на свой страх и риск".
сказки не надо рассказывать - когда там всплеск развития ИИ начался ? несколько лет назад, и ты не понимаешь очевидных вещей - ответственность за ТС и отвественность за управление ТС это пипец какие разные вещи, никто за действия водителей отвественности не несёт кроме самого водителя, а начиная с L3 производитель автомобиля должен за это нести ответственность.

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

63. Сообщение от Аноним (63), 11-Май-23, 21:00 +/–

> на всех кладбищах (enterprise environment)
Однако эти "кладбища" почему-то способны платить тебе стабильную хорошую ЗП, в отличие от "новых проектов" твоего одноклассника Васяна на модных язычках, от которых писаются кипятком все пацаны на раёне

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

64. Сообщение от Аноним (63), 11-Май-23, 21:01 +/–

Мне нравятся такие "древние" языки.
Чем меньше дешёвой школоты хочет с ней работать - тем больше моя ЗП

Ответить | Правка | Наверх | Cообщить модератору
Родитель: #40 Ответы: #65

65. Сообщение от Заноним (?), 12-Май-23, 00:28 +/–

Ну на java столько понаписали, что ЗП ещё долго будут платить.

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

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

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

Партнёры:

Хостинг:

Закладки на сайте
Проследить за страницей

Created 1996-2025 by Maxim Chirkov
Добавить, Поддержать, Вебмастеру

1. Сообщение от Аноним (1), 06-Май-23, 22:34	+/–
Скоро Фуксия со своим Цирконом спустится и покроет всё стадо.
Ответить \| Правка \| Наверх \| Cообщить модератору
Ответы: #3, #43

3. Сообщение от пох. (?), 06-Май-23, 22:38	–1 +/–
Угу, спустится, с высот фоторамки и что там еще - говорящий кофейник? Не хотел бы тебя огорчать, дружище, но это дно. С него спускаться дальше некуда. Сдохла твоя фикция, не взлетела. В принципе, конечно, от sel4 тоже толку никакого, занятный но феерично ненужный артефакт.
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #1 Ответы: #5

5. Сообщение от Аноним (1), 06-Май-23, 23:11	+1 +/–
Про джаву тоже говорили что он только для кофемашин. И где сейчас джава? Да она везде, бро!
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #3 Ответы: #36, #40

6. Сообщение от Анонн (?), 06-Май-23, 23:20	+7 +/–
Очень крутой проект, показывающий насколько тяжело и дорого так разрабатывать софт. Там всего меньше 10к строк кода ("8,700 lines of C code and 600 lines of assemble" если быть точным). При этом "затраты" на аналогичную верификацию при уже проработанной методологии - 8 (восемь) человеко-лет ("kernel plus proof of 8 py") В процессе верификации пришлось писать кучу уточнений, нашли 16 дефектов до второй фазы верификации, сама формальная верификация нашла 144 дефекта и необходимость внести 54 изменения. Т.е. где-то 1 дефект на 50 строк си/асм кода. Подробности тут: https://www.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf
Ответить \| Правка \| Наверх \| Cообщить модератору
Ответы: #7, #8, #22, #42

7. Сообщение от Аноним (1), 06-Май-23, 23:29	–1 +/–
Поэтому Hurd и не смогли дописать.
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #6 Ответы: #10

8. Сообщение от vitalif (ok), 06-Май-23, 23:32	+/–
в этом контексте "для проектов уровня промышленных операционных систем" звучит слегка забавно
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #6 Ответы: #45

9. Сообщение от InuYasha (??), 06-Май-23, 23:37	–1 +/–
Сейчас растоманы не просто нервно курят в сторонке, а задыхаются в дыму, дёргаясь в припадках )
Ответить \| Правка \| Наверх \| Cообщить модератору
Ответы: #11, #16

10. Сообщение от пох. (?), 07-Май-23, 00:10	–2 +/–
Нет, его к счастью писали, а не верифицировали-верифицировали. Просто на фоне линукса это неповоротливое чудовище (с драйверами, как нельзя более кстати, копипащенными из линукса же) оказалось никому совершенно не нужным. Т.е. добились что оно загружалось и можно было даже набрать /bin/ls - но что делать дальше все равно никто не знал. А это недоразумение даже и такого не может.
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #7

11. Сообщение от пох. (?), 07-Май-23, 00:11	+2 +/–
Ну если честно - их ресдох хотя бы был похож на законченую операционную систему. А тут голое микроядро непонятно для чего, зато верифицированное.
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #9 Ответы: #12, #13

12. Сообщение от Аноним (12), 07-Май-23, 01:01	–1 +/–
Почему "непонятно для чего"? Как раз понятно - чтобы использовать его как запускалку виртуальных машин и быть уверенным что не выйдет за пределы виртуалки. "seL4 can run Linux in a virtual machine. seL4 is [...] hypervisor with a sound worst-case execution-time (WCET) analysis, and as such the only one that can give you actual real-time guarantees, no matter what others may be claiming."
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #11 Ответы: #18, #26

13. Сообщение от tty0 (?), 07-Май-23, 01:03	+/–
Проблема в том, что людей, которым нужен не продукт, а инструмент слишком мало. На этом проекте можно реализовать очень крутые вещи, к примеру, захардкодив ядро целиком в железе. Но это слишком долго, а значит будем по старинке - нестабильное ядро и много обновлений
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #11

16. Сообщение от Прохожий (??), 07-Май-23, 02:08	–5 +/–
С логикой и здравым смыслом у очередного местного аналитика (от слова анал) всё, как обычно, то есть никак. Если уж кто и будет задыхаться и дёргаться в припадках, так это Сишники. 9 тыс. строк кода и 8 лет верификации - прекрасная производительность (нет). Не говоря уж о стоимости. Куда лучше всё-таки, когда от подавляющей части ошибок защищает компилятор прямо во время разработки. Остальные верифицировать займёт куда меньше времени.
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #9 Ответы: #27

18. Сообщение от Аноним (18), 07-Май-23, 03:56	+/–
Осталось ешё верифицированную виртулку написать. Если неверифицированную, то можно Genode взять.
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #12

22. Сообщение от Аноним (22), 07-Май-23, 08:33	–1 +/–
верификация Слово "проверка" ведь с более меньшим углеродным следом, товарищи.. )
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #6 Ответы: #41

24. Сообщение от Аноним (24), 07-Май-23, 08:54	+/–
Они что-то там на Haskell начудили, молодцы. А я могу таким же образом мой код верифицировать? У меня есть несколько крошечных проектов, на тысячу строк.
Ответить \| Правка \| Наверх \| Cообщить модератору
Ответы: #61

26. Сообщение от пох. (?), 07-Май-23, 09:55	+1 +/–
> Почему "непонятно для чего"? > Как раз понятно - чтобы использовать его как запускалку виртуальных машин и для запускалки виртуальных машин общего назначения а не чего-то совсем не от мира сего - надо уметь в сети, диски, межхостовый обмен, паравиртуализацию и Б-г знает чего еще кажущееся очевидным я забыл. А тут ничего нет, пустыня. > быть уверенным что не выйдет за пределы виртуалки. виртуалка без сети, дисков и управления и так никуда не выйдет, а выйдет так пожалеет что вышла - потому что там опять ничегошеньки нет. То есть написать это все (неизвестно, между нами, с какой итоговой производительносью и куда при этом пойдет верифицированность) наверное можно, но нереально - нет у человечества столько лишних кодеров. Остаются только совсем уж странные нишевые применения, а поскольку те никогда не будут массовыми - рынок и в этих нишах выберет что попроще и попонятнее.
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #12

27. Сообщение от пох. (?), 07-Май-23, 09:58	+/–
> Куда лучше всё-таки, когда от подавляющей части ошибок защищает компилятор прямо во > время разработки. Остальные верифицировать займёт куда меньше времени. да, просто прекрасно. Все время разработки уходит на борьбу с компилятором, потом чувак сдается и пишет unsafe {мамойклянус!} Результат - компилятор успешно защитил, нет разработки нет и ошибок. Не правда ли, ресдох?
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #16

29. Сообщение от Аноним (29), 07-Май-23, 12:48	+/–
> вручается за разработку программных систем, оказавших определяющее влияние на отрасль шта?! А можно чуть подробнее, на что повлияла разработка seL4? Может, какие-то ОС на ней написали годные? Хотя бы уровня Линукса - 1% декстопа и то хорошо. Или seL4 только тем и хороша, что про неё ГОДАМИ только и можно писать, что она "верифицируемая"? :))))))) (проверяемая, клоуны!)
Ответить \| Правка \| Наверх \| Cообщить модератору
Ответы: #31, #32, #33, #44

31. Сообщение от Аноним (31), 07-Май-23, 13:47	–1 +/–
https://www.opennet.ru/opennews/art.shtml?num=59052 Это Вам не подойдет?
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #29

32. Сообщение от пох. (?), 07-Май-23, 16:34	+/–
> А можно чуть подробнее, на что повлияла разработка seL4? "Болгары восхитились!" Ну и вообще, чего докопался, это не троллейбус из буханки, это корабль в бутылке в форме буханки. Кросивое! Поставить в музей на центральное место экспозиции, ходить вокруг на цыпочках, умиляться. Потом, когда-нибудь, обнаружим что интел впилил ее в ядро своего ME заместо нынешнего (тоже троллейбуса но гораздо менее выдающегося) или еще где в подобном месте всплывет. > (проверяемая, клоуны!) этому - десять плетей за иноземные слова воспрещенные. Не клоуны, а скоморохи! Клоуны - это когда в DF докопался до адамантина на один лишний кубик.
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #29

33. Сообщение от Степан (?), 07-Май-23, 19:02	+/–
> декстопа > проверяемая, клоуны
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #29 Ответы: #35

34. Сообщение от fidoman (ok), 07-Май-23, 19:45	–2 +/–
Строгое математическое доказательство показало, что все предусмотренные ТЗ бекдоры на месте.
Ответить \| Правка \| Наверх \| Cообщить модератору

35. Сообщение от пох. (?), 07-Май-23, 21:54	+1 +/–
О, точно, двадцать плетей басурманину! Столешница, скоморох!
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #33

36. Сообщение от _ (??), 08-Май-23, 04:15	+/–
Ну да - на всех кладбищах (enterprise environment). Новых проектов на ней нет. Как и предсказывалось - новый Кобол :(
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #5 Ответы: #38, #63

38. Сообщение от Аноним (38), 08-Май-23, 08:49	–1 +/–
Ксожалению, таки есть. Для новых прозектов берут Швинг и продолжают пейсать на джяве. И логика в этом есть, и есть причины так делать.
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #36 Ответы: #39

39. Сообщение от Аноним (39), 08-Май-23, 11:20	+1 +/–
А чем Котлин не джава?
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #38

40. Сообщение от Заноним (?), 08-Май-23, 18:51	+/–
Да не везде, и вообще она давно закатывается. И даже graalvm её не вытянет. Как ранее сказали - очередной cobol.
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #5 Ответы: #64

41. Сообщение от Аноним (41), 08-Май-23, 19:24	+5 +/–
Верификация - проверка Аутентификация - проверка Авторизация - проверка Валидация - проверка
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #22

42. Сообщение от warlock66613 (ok), 08-Май-23, 20:58	+/–
Интересные подробности. Я особенно обратил бы внимание на то, что 1) это всё пока без поддержки многоядерности/мультипроцессорности, 2) им пришлось жёстко отказаться от указателей на стек: если в коде указатель, то его цель — в куче. Довольно серьёзные ограничения, особенно если подумать о них вместе.
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #6

43. Сообщение от Аноним (43), 08-Май-23, 21:36	+1 +/–
> Скоро Фуксия у гугла и на sel4 есть ОС https://www.opennet.ru/opennews/art.shtml?num=57920
Ответить \| Правка \| Наверх \| Cообщить модератору
Родитель: #1