| |
| 2.3, пох. (?), 22:38, 06/05/2023 [^] [^^] [^^^] [ответить]
| –1 +/– | |
Угу, спустится, с высот фоторамки и что там еще - говорящий кофейник?
Не хотел бы тебя огорчать, дружище, но это дно. С него спускаться дальше некуда. Сдохла твоя фикция, не взлетела.
В принципе, конечно, от sel4 тоже толку никакого, занятный но феерично ненужный артефакт.
| | |
| |
| 3.5, Аноним (1), 23:11, 06/05/2023 [^] [^^] [^^^] [ответить]
| +1 +/– |
Про джаву тоже говорили что он только для кофемашин. И где сейчас джава? Да она везде, бро!
| | |
| |
| 4.36, _ (??), 04:15, 08/05/2023 [^] [^^] [^^^] [ответить]
| +/– |
Ну да - на всех кладбищах (enterprise environment). Новых проектов на ней нет. Как и предсказывалось - новый Кобол :(
| | |
| |
| 5.38, Аноним (38), 08:49, 08/05/2023 [^] [^^] [^^^] [ответить]
| –1 +/– |
Ксожалению, таки есть. Для новых прозектов берут Швинг и продолжают пейсать на джяве. И логика в этом есть, и есть причины так делать.
| | |
| 5.63, Аноним (63), 21:00, 11/05/2023 [^] [^^] [^^^] [ответить]
| +/– | |
> на всех кладбищах (enterprise environment)
Однако эти "кладбища" почему-то способны платить тебе стабильную хорошую ЗП, в отличие от "новых проектов" твоего одноклассника Васяна на модных язычках, от которых писаются кипятком все пацаны на раёне
| | |
|
| 4.40, Заноним (?), 18:51, 08/05/2023 [^] [^^] [^^^] [ответить]
| +/– |
Да не везде, и вообще она давно закатывается. И даже graalvm её не вытянет.
Как ранее сказали - очередной cobol.
| | |
| |
| 5.64, Аноним (63), 21:01, 11/05/2023 [^] [^^] [^^^] [ответить]
| +/– |
Мне нравятся такие "древние" языки.
Чем меньше дешёвой школоты хочет с ней работать - тем больше моя ЗП
| | |
|
|
|
|
| 1.6, Анонн (?), 23:20, 06/05/2023 [ответить] [﹢﹢﹢] [ · · · ]
| +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
| | |
| |
| |
| 3.10, пох. (?), 00:10, 07/05/2023 [^] [^^] [^^^] [ответить]
| –2 +/– | |
Нет, его к счастью писали, а не верифицировали-верифицировали.
Просто на фоне линукса это неповоротливое чудовище (с драйверами, как нельзя более кстати, копипащенными из линукса же) оказалось никому совершенно не нужным.
Т.е. добились что оно загружалось и можно было даже набрать /bin/ls - но что делать дальше все равно никто не знал.
А это недоразумение даже и такого не может.
| | |
|
| 2.8, vitalif (ok), 23:32, 06/05/2023 [^] [^^] [^^^] [ответить]
| +/– |
 в этом контексте "для проектов уровня промышленных операционных систем" звучит слегка забавно
| | |
| |
| 3.45, пох. (?), 23:09, 08/05/2023 [^] [^^] [^^^] [ответить]
| +/– | |
промышленная - это в промышленности. Каким-нибудь приводом конвейера управлять, с положением на две позиции - заготовка едет и заготовка стоит.
Или еще что незамысловатое. Тут верю, вполне годится. Ну если pic какой слишком сложно этим озадачить.
| | |
|
| 2.22, Аноним (22), 08:33, 07/05/2023 [^] [^^] [^^^] [ответить]
| –1 +/– | |
верификация
Слово "проверка" ведь с более меньшим углеродным следом, товарищи.. )
| | |
| |
| 3.41, Аноним (41), 19:24, 08/05/2023 [^] [^^] [^^^] [ответить]
| +5 +/– |
Верификация - проверка
Аутентификация - проверка
Авторизация - проверка
Валидация - проверка
| | |
|
| 2.42, warlock66613 (ok), 20:58, 08/05/2023 [^] [^^] [^^^] [ответить]
| +/– |
 Интересные подробности. Я особенно обратил бы внимание на то, что 1) это всё пока без поддержки многоядерности/мультипроцессорности, 2) им пришлось жёстко отказаться от указателей на стек: если в коде указатель, то его цель — в куче. Довольно серьёзные ограничения, особенно если подумать о них вместе.
| | |
|
| 1.24, Аноним (24), 08:54, 07/05/2023 [ответить] [﹢﹢﹢] [ · · · ]
| +/– | |
Они что-то там на Haskell начудили, молодцы.
А я могу таким же образом мой код верифицировать?
У меня есть несколько крошечных проектов, на тысячу строк.
| | |
| |
| 2.61, warlock66613 (ok), 12:16, 10/05/2023 [^] [^^] [^^^] [ответить]
| +/– |
Нет. Вы же наверняка используете сторонние библиотеки, как минимум стандартную библиотеку.
| | |
|
| 1.29, Аноним (29), 12:48, 07/05/2023 [ответить] [﹢﹢﹢] [ · · · ]
| +/– | |
> вручается за разработку программных систем, оказавших определяющее влияние на отрасль
шта?! А можно чуть подробнее, на что повлияла разработка seL4? Может, какие-то ОС на ней написали годные? Хотя бы уровня Линукса - 1% декстопа и то хорошо. Или seL4 только тем и хороша, что про неё ГОДАМИ только и можно писать, что она "верифицируемая"? :))))))) (проверяемая, клоуны!)
| | |
| |
| 2.32, пох. (?), 16:34, 07/05/2023 [^] [^^] [^^^] [ответить]
| +/– | |
> А можно чуть подробнее, на что повлияла разработка seL4?
"Болгары восхитились!"
Ну и вообще, чего докопался, это не троллейбус из буханки, это корабль в бутылке в форме буханки. Кросивое! Поставить в музей на центральное место экспозиции, ходить вокруг на цыпочках, умиляться. Потом, когда-нибудь, обнаружим что интел впилил ее в ядро своего ME заместо нынешнего (тоже троллейбуса но гораздо менее выдающегося) или еще где в подобном месте всплывет.
> (проверяемая, клоуны!)
этому - десять плетей за иноземные слова воспрещенные.
Не клоуны, а скоморохи!
Клоуны - это когда в DF докопался до адамантина на один лишний кубик.
| | |
| |
| 3.35, пох. (?), 21:54, 07/05/2023 [^] [^^] [^^^] [ответить]
| +1 +/– | |
О, точно, двадцать плетей басурманину! Столешница, скоморох!
| | |
|
| 2.44, Аноним (43), 21:47, 08/05/2023 [^] [^^] [^^^] [ответить]
| +1 +/– | |
> на что повлияла разработка seL4?
на разработку современных систем применяемых в критически важных областях - автомобильной, медицинской, аерокосмической, военной. Сейчас майнстрим - гипервизор на клонах L4, см например
https://en.wikipedia.org/wiki/PikeOS
| | |
| |
| 3.46, пох. (?), 23:17, 08/05/2023 [^] [^^] [^^^] [ответить]
| +/– | |
чегой-то мне кажется что мэйнстрим сейчас - как в тойете с педалью газа. Когда при наличии двухканального датчика индус ляпает еще один китайский глючный (потому что не знает про второй канал или не умеет вообще в тот датчик) а потом кодит такое что счастливый клиент убивается апстену. Всем похрену.
https://en.wikipedia.org/wiki/PikeOS
It enables users to build certifiable smart devices for the Internet of things (IoT)
Т.е. и этим прекрасным микроскопом просто забивают гвозди.
Ну в общем логично, учитывая eclipse и прочий трэшачок.
| | |
| |
| 4.47, Аноним (43), 10:27, 09/05/2023 [^] [^^] [^^^] [ответить]
| +/– | |
> мне кажется что мэйнстрим сейчас - как в тойете с педалью газа
майнстрим сейчас исключить человеческий фактор из управления автомобилями
https://www.mobileye.com/
> Т.е. и этим прекрасным микроскопом просто забивают гвозди
они зарабатывают на всём, денег больше всего в ширпотребе. В автомобилях выпускаемых в Германии используют открытый фреймворк l4re
https://www.kernkonzept.com
| | |
| |
| 5.48, пох. (?), 11:28, 09/05/2023 [^] [^^] [^^^] [ответить]
| +/– | |
Ну вот тойета опередила тренд на десять лет. Правда, "исключенному" человеческому фактору кажется не очень понравилось вляпываться в стену.
| | |
| 5.49, Аноним (49), 12:37, 09/05/2023 [^] [^^] [^^^] [ответить]
| +1 +/– |
 > майнстрим сейчас исключить человеческий фактор из управления автомобилями
> https://www.mobileye.com/
Майстрим сейчас, как и всегда - подоить доверчивых лошк^W инвесторов и потребляd^Hтелей.
Маск вон, уже почти десять лет - "еще немного и уже почти совсем скоро" и ниче, пипл хавает за обе щеки.
А в реальности, хорошо если лет через 15-20 что-то не сильно стремное в этой области появится.
| | |
| |
| 6.52, пох. (?), 15:24, 09/05/2023 [^] [^^] [^^^] [ответить]
| +/– |
Ну зочем вы тгавите - Маск всего двух только пока и убил. (Ну трех если считать отправленного в космос с билетом в один конец)
| | |
| 6.54, Аноним (43), 16:25, 09/05/2023 [^] [^^] [^^^] [ответить]
| +/– | |
> Майстрим сейчас, как и всегда - подоить доверчивых лошк^W инвесторов и потребляd^Hтелей.
для развития технологий нужны финансы это очевидно, но вы покупаете товары потому что лош.к ? а я думаю что для собственного комфорта. Но конечно можете и на собачках скакать вместо автомобилей. И ж..у берестой подтирать, бумага для лошк.в
| | |
| |
| 7.55, Аноним (49), 17:16, 09/05/2023 [^] [^^] [^^^] [ответить] | +/– | А в огороде бузина, это тоже очевидно Внезапно, можно развивать технологии и пр... большой текст свёрнут, показать | | |
| |
| 8.59, Аноним (43), 23:28, 09/05/2023 [^] [^^] [^^^] [ответить] | +/– | внезапно переход от L2 к L3 имеет чисто правовые сложности - после сертификации ... текст свёрнут, показать | | |
| |
| 9.60, Аноним (49), 11:37, 10/05/2023 [^] [^^] [^^^] [ответить] | +1 +/– | Угу, чисто правовые сложности опять танцорам мешают, а не то они бы всем показ... большой текст свёрнут, показать | | |
| |
| 10.62, Аноним (43), 09:31, 11/05/2023 [^] [^^] [^^^] [ответить] | –1 +/– | сказки не надо рассказывать - когда там всплеск развития ИИ начался несколько ... текст свёрнут, показать | | |
|
|
|
|
|
|
| 4.51, Аноним (51), 14:04, 09/05/2023 [^] [^^] [^^^] [ответить] | –2 +/– |  с моей точки зрения вся эта идея формальной верификации микроядра и полученной з... большой текст свёрнут, показать | | |
| |
| 5.53, пох. (?), 15:26, 09/05/2023 [^] [^^] [^^^] [ответить]
| +1 +/– | |
поток сознания эксперта опеннета
Про то что такое формальная верификация и как это работает - читать ему разумеется, не интересно и незачем, у него уже есть ценное мнение.
| | |
|
|
|
|
| 1.34, fidoman (ok), 19:45, 07/05/2023 [ответить] [﹢﹢﹢] [ · · · ]
| –2 +/– |
 Строгое математическое доказательство показало, что все предусмотренные ТЗ бекдоры на месте.
| | |
| 1.50, Аноним (51), 14:03, 09/05/2023 [ответить] [﹢﹢﹢] [ · · · ]
| –4 +/– |
лично мне чужды подобные инновационные решения встроеных систем, я предпочитаю разрабатывать прикладные решения на языке си-плюсплюс в среде майкрософт визуал студио, а для моих задач со средней нагрузкой предпочтительнее простой монолитный ядренной архитектуры виндовс,которая проверенная временем и хорошо изученная, а эти "легковесные" микроядра только усложняют работу без очевидных преимуществ для обычного прикладного разработчика,как говорится "если не сломалось - не чини" и кто то явно преувеличивает значимость этого проекта чтобы получить гранты и деньги, поэтому я не вижу ничего выдающегося в этом проекте и его награждении
| | |
|
