| |
| |
| |
| 4.29, МарьВанна (?), 06:17, 26/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| –14 +/– | |
Математическая верификация не спасает от ошибок в коде. Математическая верификация - это просто игрушка академиков и профессоров.
Только чистый Си.
| | |
| 4.36, Онаним (?), 07:31, 26/10/2021 [^] [^^] [^^^] [ответить] [↓] [к модератору]
| +3 +/– |
"Математическая верификация" гарантирует только, что оно не слетит в UB или runtime error. От разрушительного поведения в силу логических ошибок она не спасает.
| | |
| |
| |
| 6.57, Онаним (?), 09:48, 26/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| +/– |
А смысл?
Оно всё равно всё так же при неудачном раскладе звёзд может например потерей данных кончиться, просто в другом месте.
| | |
|
| |
| 6.83, Совершенно другой аноним (?), 12:34, 26/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| –1 +/– |
см сообщения #43 - для SeL4, который на C тоже делали "Математическую верификацию". И по-моему там тоже использовалось подмножество языка C, но его никто не называл красивыми словами SPARK-2014 или как-то ещё.
| | |
| |
| 7.88, Аноним (-), 12:46, 26/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| +3 +/– |
> см сообщения #43 - для SeL4, который на C тоже делали "Математическую
> верификацию". И по-моему там тоже использовалось подмножество языка C,
Писали на самом деле на хаскеле, лишь после верификации корректности логики работы транслируя в сишку. И обошлась та верификация где-то в 20 человеко-лет на 9000 строк кода. А так да, все с Великой Сишкой хорошо и все придумки нового - от лукавого!
| | |
|
|
|
|
| 3.25, Аноньимъ (ok), 04:10, 26/10/2021 [^] [^^] [^^^] [ответить] [↑] [к модератору]
| –10 +/– |
 Это какая-то новая стадия отрицания.
Сишка это помойный язык с нездоровым синтаксисом, околонулевой семантикой, и фрагментированой инфраструктурой.
На котором можно просто и быстро писать системное ПО невероятно низкого качества.
| | |
| |
| 4.54, sdfgjsdfjdj (?), 09:39, 26/10/2021 [^] [^^] [^^^] [ответить] [↓] [к модератору]
| +2 +/– |
Си - это ассемблер для ленивых. он легко позволяет делать реализации всяких resource-critical вещей, вплоть до того, что можно предсказать сколько тактов процессора займёт исполнение кода, за это его и любят
| | |
| |
| 5.84, Аноним (-), 12:36, 26/10/2021 [^] [^^] [^^^] [ответить] [↑] [к модератору]
| +/– |
> вплоть до того, что можно предсказать сколько тактов процессора
> займёт исполнение кода, за это его и любят
Скорее - вплоть до самых разных баек о том, "как можно суперкруто".
| | |
| 5.107, Аноньимъ (ok), 15:51, 26/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| –1 +/– | |
>Си - это ассемблер для ленивых. он легко позволяет делать реализации всяких resource-critical вещей, вплоть до того, что можно предсказать сколько тактов процессора займёт исполнение кода
Yes.
>за это его и любят
Любят его престарелые смузихлебы за то-же за что молодые любят жаваскрипт.
| | |
|
| 4.94, uis (ok), 12:59, 26/10/2021 [^] [^^] [^^^] [ответить] [↑] [к модератору]
| –2 +/– |
 > На котором можно просто и быстро писать системное ПО невероятно низкого качества.
При чём тут питон? А, тьфу, питон про прикладное ПО невероятно низкого качества.
Может тебе ещё и в асме синтаксис нужен? А какой, at&t или intel? Или лучше ради единственно-верного карго-культа собирать компилятор на десяток-другой гигов места под объектники и восемь гигов исходников?
| | |
| |
| 5.108, Аноньимъ (ok), 15:58, 26/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| –1 +/– | |
>При чём тут питон? А, тьфу, питон про прикладное ПО невероятно низкого качества.
Да, сишка это системный питон такой. Врайт ванце краш еверивере.
>Может тебе ещё и в асме синтаксис нужен?
В сишке синтаксиса очень очень дофига. Я никогда не говорил что в сишке не хватает синтаксиса.
Речь шла о том, что он ужасный, и лишённый семантики.
>А какой, at&t или intel? Или лучше ради единственно-верного карго-культа собирать компилятор на десяток-другой гигов места под объектники и восемь гигов исходников?
Чё? Да, GCC ужасный монстр, я согласен. Монструозность GCC, к которому ещё и систему сборки нужно отдельно прикручивать, и систему управления пакетами, хорошо демонстрирует мною сказанное.
| | |
| |
| 6.127, Онаним (?), 19:57, 26/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| +/– |
> В сишке синтаксиса очень очень дофига. Я никогда не говорил что в сишке не хватает синтаксиса.
> Речь шла о том, что он ужасный, и лишённый семантики.
Лучше и читабельнее пока не придумано, все эти питорастические извраты так извратами и останутся.
Нет, из сей тоже можно сделать троллейбус, как из той буханки, но если писать не ради извращения - будет читабельно.
| | |
|
|
|
|
| |
| 3.24, Аноньимъ (ok), 04:05, 26/10/2021 [^] [^^] [^^^] [ответить] [↓] [к модератору]
| +2 +/– |
Потому, что Ада куда более структурирована, детерминирована, и поддаётся верификации.
К тому же за Адой стоят промышленные стандарты.
Без которых, ваши заявления о надёжности вашего ПО в контексте критических задачь, ничего не стоят.
| | |
| |
| 4.99, YetAnotherOnanym (ok), 13:58, 26/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| –1 +/– |
 > твой объект ненависти за год то этого был еще в пеленках и непонятно чем
Дык отож - пока сабж пилили, оно так и не стало ничем таким, что могло бы перетянуть к себе разработчиков и побудить их отказаться от Ады.
| | |
|
|
|
| |
| 2.3, Онаним (?), 22:13, 25/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| +8 +/– |
Э-э-э, а какой в этом смысл?
Если возникла ситуация, в которой только реакция watchdog поможет - сохранять что-то уже поздно, и небезопасно - есть риск данных лишиться.
| | |
| |
| 3.33, Аноним (33), 07:04, 26/10/2021 [^] [^^] [^^^] [ответить] [↓] [к модератору]
| –1 +/– |
смысл зависит от реализации. Вызов вачдога может запустить полную проверку контекстов. Получим надежность в целом с минимальными потерями. По крайней мере в контроллерах это прокатывает, хотя в ос конечно сложней.
| | |
| |
| 4.35, Онаним (?), 07:29, 26/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| +3 +/– |
Единственный смысл - снять дамп/бектрейс (опционально) и перезапуститься.
Никакая "полная проверка контекстов" не выявит причин вставания системы раком.
Либо будет сложнее и затратнее самой системы.
А если потенциальные причины известны и есть ресурсы на создание "проверки контекстов" - проще вложить их собственно в устранение этих причин.
| | |
| 4.92, uis (ok), 12:53, 26/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| +/– | |
> Вызов вачдога может запустить полную проверку контекстов.
Если это он, то не может. Он должен делать аппаратный сброс.
| | |
| 4.110, Аноним (33), 16:14, 26/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| +/– |
да успокойтесь уже, не говорится в этой оси про вачдог. Речь была о контроллере. Была необходимость и было так сделано. Какие блин виртуалки?
| | |
|
|
|
| 1.6, QwertyReg (ok), 22:32, 25/10/2021 [ответить] [﹢﹢﹢] [ · · · ] [↓] [↑] [к модератору]
| –5 +/– |
 > Ядро доступно для архитектуры x86_64
То есть даже тут x86 слили в отстойник истории. А кто-то до сих пор над десктопе насилует труп, лол.
| | |
| |
| 2.12, Аноним (12), 22:40, 25/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| –4 +/– | |
Действительно, сейчас все бросятся на твой растопроц
А я думал уже глупее фрактала с лошадкой быть не может. Но тут появился ты.
| | |
| 2.13, пончик (?), 22:43, 25/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| –3 +/– | |
И как же ты по такой фразе сделал такой вывод?
Ты бы с наркотой завязал а? пока не поздно. Или уже поздно и мозг проржавел?
| | |
|
| |
| |
| 3.61, pofigist (?), 10:09, 26/10/2021 [^] [^^] [^^^] [ответить] [↓] [к модератору]
| +4 +/– |
Да-да-да!
Коричневая обложка...
Еду как-то на 22м троллейбусе мимо елоховки - тогда в этом поповнике весь цвет РПЦ отирался... Читаю эту книжку... А рядом - куча воцерквленных бабок...
Представляете какой цирк с конями начался, когда я книжку закрыл и они прочитали ее название? 🤣
| | |
|
|
| |
| 2.31, Аноним (31), 06:26, 26/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| +/– | |
>В образах компонентов с Linux задействовано ядро Linux 5.4.66.
Муэн - микроядро. А Линукс- это и ещё сброник аппаратных и виртуальных драйверов.
| | |
| |
| |
| |
| |
| |
| 7.81, pofigist (?), 12:11, 26/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| –1 +/– | |
Нда... у 3.11 - микроядро... учи матчасть!
Лучше как у линакса - когда в процессе установки надо качать все окружение... если сеть подымется. netinstall ога :)
| | |
|
|
|
| 4.87, uis (ok), 12:45, 26/10/2021 [^] [^^] [^^^] [ответить] [↑] [к модератору]
| +/– |
Угу. И количество переключений контекста тоже здоровенного человека. Особенно это весело с использованием приёмчиков предотвращения утечек по сторонним каналам.
| | |
|
|
|
| |
| 2.39, . (?), 08:20, 26/10/2021 [^] [^^] [^^^] [ответить] [↓] [к модератору]
| –2 +/– | |
Ненужная ос на ненужном языке - с ненужной лицензией, все правильно.
Кто-то защитил свой phd, и можно выносить.
| | |
| |
| 3.59, Онаним (?), 09:49, 26/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| +1 +/– |
Ну почему ненужная-то.
Да, академическая поделка.
Но с учётом проделанной работы по верификации секущихся концов (не алгоритмической конечно...), вполне себе годно, только не знаю, для чего.
| | |
| |
| 4.69, пох. (?), 11:00, 26/10/2021 [^] [^^] [^^^] [ответить] [↓] [к модератору]
| –2 +/– | |
Ну вот это и есть синоним ненужного - "годно не знаю для чего".
Поскольку запустить из реально существующего можно только кастрированный линукс, а зачем нам еще один?
| | |
| |
| 5.71, Аноним (68), 11:08, 26/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| –1 +/– | |
А тем временем, на SPARK-2014, под Muen OS, люди в Европе потихоньку переписывают код с C и Rust..
Решения есть, где нужна высокий уровень безопасности, стабильности и работы в режиме реального времени.
| | |
|
| 4.70, Аноним (68), 11:03, 26/10/2021 [^] [^^] [^^^] [ответить] [↑] [к модератору]
| +/– | |
Люди на Muen OS давно девайсы выпускают, например такой: https://www.nitrokey.com/products/nethsm Меня повеселила одна фича: "наш девайсы с OS настолько безопасны, что даже консоль для ввода и вывод на монитор не предусмотрены..."
Гениально! Зачем компу клава и монитор? Еще и админа тогда надо чтоб сидел и стучал по клаве, смотрел в монитор. Комп должен просто работать, без человека, как лампочка, включил и оно работает.
| | |
|
|
|
| 1.42, . (?), 08:23, 26/10/2021 [ответить] [﹢﹢﹢] [ · · · ] [↑] [к модератору]
| –1 +/– | |
> Система непрерывной интеграции переведена с эмулятора Bochs на вложенные окружения QEMU/KVM.
все что нужно знать об этой бесполезной поделке.
| | |
| |
| |
| |
| 4.117, Аноним (-), 17:12, 26/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| +/– |
Старые программисты на Ада умрут от старости, без модной молодёжи кому вы свою Адскую Отчизну оставите? Или думаете, как в Дебиане, на вашу сторону появится поток из стареющих пацанов?
| | |
|
|
|
| |
| 2.124, Аноним (-), 18:37, 26/10/2021 [^] [^^] [^^^] [ответить] [↓] [к модератору]
| +/– |
многаденех курсы бисплатные личная пальма под цвет ноутбука ада за 24 часа от нуля до гираскутера гламурная барада в пакете с первой дозой в падарок
| | |
| |
| 3.133, Аноним (-), 06:31, 27/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| +/– | |
Райдер модного, молодёжного и прогрессивного человека.
1. Много денег.
2. Бесплатные курсы по языку Ада.
3. Свой остров, или пляж с пальмами под цвет ноутбука.
4. Книжка "Освой Ада за 24 часа".
5. Гироскутер.
6. Гламурная борода.
7. Доза веществ в пакете (в подарок). Нужно для того чтобы возникали в голове творческие мысли.
В принципе всё, юридически оформил. Пунк 7 хорошо реализуем в Калифорнии, либо в Нидерландах.
| | |
|
| 2.147, Аноним (33), 17:08, 27/10/2021 [^] [^^] [^^^] [ответить] [↑] [к модератору]
| +/– |
Аду же разрабатывала оборонка америки. Наса на ней клепала управление своими шатлами. Помнится трапалась на пуске по каждому чиху. Но работала вроде надежно. Программисты на ней писали кажется только для ихнего впк, про гражданские проекты не слышно было
| | |
|
| 1.131, Gogi (??), 20:30, 26/10/2021 [ответить] [﹢﹢﹢] [ · · · ] [↓] [↑] [к модератору]
| +/– |
Мне от одного списка (аппаратных) возможностей плохо стало! Неужели ВСЁ ЭТО нужно для того, чтобы юзер тупо запустил ворд?? (условно говоря)
По-моему, проектировщики аппаратуры стали такой же тупой индуснёй, как и в софте - главное наструячить побольше фич, а надо оно или нет - да пофиг, оплачено! (как было с x86 + защищённый режим + тонна сопутствующих НЕНУЖНЫХ регистров, таблиц и т.п.)
Гениальное обязано быть простым и понятным. Если какую-то платформу раздули до неосязаемых архитектурных громад, нахрен такую архитектуру. Я лучше на БК0010 буду редактировать, чем на суперзащищённом x86 ждать, когда меня вскроют через IME.
| | |
| |
| 2.145, Аноним (142), 12:48, 27/10/2021 [^] [^^] [^^^] [ответить] [к модератору]
| +/– |
сперва академическое открытое, потом уж точное наведение на нужную голову в реалтайм. но цена головы/репутации с нулевых сильно упала, потому можно и гражданским линуксом по квадрату с задержкой и осечкой.
| | |
|
|
