[00:17:20] <ada_ru> (Oleg) https://www.aex.ru/news/2020/1/14/207102/
[00:19:14] <ada_ru> (I_vlxy_I) таким образом сотрудники боинга убили несколько сот человек
[00:19:22] <ada_ru> (Oleg) Мудаки
[00:23:03] <ada_ru> (Oleg) Сделал как обычно на скорую руку на Go утилиту
[00:23:21] <ada_ru> (Oleg) Go это какой то наркотик/вирус
[00:23:51] <ada_ru> (Oleg) Завтра на Ada начну 😊
[00:24:13] <ada_ru> (Oleg) У меня тут идея родиласть - завтра расскажу
[00:27:26] <ada_ru> (Oleg) Как вам такой стиль ReadMe?
[00:27:55] <ada_ru> (Oleg) <прислал документ>
[00:32:11] <ada_ru> (Лекс) красиво но практичность страдает, имхо
[00:34:15] <ada_ru> (Oleg) Да надо покрупнее и со ссылками
[00:34:30] <ada_ru> (Oleg) Завтра поделаю
[00:35:01] <ada_ru> (Oleg) Сделал утилиту сборки данных с кучи коммутаторов мультивенлорных
[00:43:15] <ada_ru> (Лекс) там шрифты плохо читаются
[00:43:55] <ada_ru> (Лекс) ток это ж на перле можно было по быстрому состряпать 😃 зачем ещё го какой-то
[00:55:23] <ada_ru> (Oleg) На perl если только с помощью net-snmp и такой то матери
[00:55:32] <ada_ru> (Oleg) Там не все так просто
[00:56:30] <ada_ru> (Oleg) А тут самодостаточные утилиты под Win/Linux/MAC и не надо ничего писать самому
[00:58:21] <ada_ru> (Oleg) Ну и есть особенности - Если есть телефоны Avaya - показыапется его номер , имя абонента и модель
[00:58:39] <ada_ru> (Oleg) Этого пока в доке нет
[00:58:48] <ada_ru> (Oleg) На дгях покажу
[01:06:20] <ada_ru> (Oleg) отвечает (Лекс) на <ток это ж на перле м…>
И это:
[01:06:42] <ada_ru> (Oleg) картинка https://www.ada-ru.org/files/bot/2020-01-14-x1.jpg
[01:07:01] <ada_ru> (Oleg) Perl же теперь Раку или Раком как там его 😊
[01:07:20] <ada_ru> (Лекс) раку это не перл, перл это перл 😃
[01:08:25] <ada_ru> (Лекс) два языка, как c и c++
[01:09:10] <ada_ru> (Oleg) Да? ну может быть - я его так, иногда вижу и матерюсь хотя на нем многое очень неплохо делается
[01:11:42] <ada_ru> (Oleg) Цисковские пароли тип 7 декодер на перле правил - и написал в итоге свой на Go 😊
[01:18:04] <ada_ru> (Oleg) Уолл — автор клиента Usenet и широкоиспользуемой программы patch. Он дважды побеждал в международном конкурсе запутанного кода на языке программирования Си 😊 он начал тренироваться еще в C
[03:18:47] <ada_ru> (Лекс) https://habr.com/ru/post/483864/
[08:28:47] <ada_ru> (Oleg) Все тесты производительности C++ vs any начинаются с вектора :-) и везде на плюсах код кривой, с питоном тоже был фейл - питон оказался быстрее
[08:29:11] <ada_ru> (Oleg) Правда модификация кола на плюсах все расставила по местам
[10:31:10] <ada_ru> (I_vlxy_I) Даёшь реализацию на Аде!
[10:40:47] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Даёшь реализацию на …>
Можно, но зачем? :)
Ада же не для выжимания капелек перформанса
[10:48:18] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Можно, но зачем? :)
…>
Ну, как минимум она должна быть быстрее хаскелля и всяких шарпов-яв. По крайней мере с опцией -gnatp
[10:56:47] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Ну, как минимум она …>
Тут от задач зависит. Хаскель иногда может быть очень быстрым, что собственно тот тест и показал. Ада с выключенными проверками на простых задачах будет на уровне сишника/плюсов - бэкенд-то одинаковый (gcc/llvm)
[10:57:33] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Тут от задач зависит…>
Код генерируется немного другой все равно. Некоторые проверки не отключить
[10:59:50] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Код генерируется нем…>
А какие проверки не отключить?
Я думал при желании можно все их вырубить
[11:05:53] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <А какие проверки не …>
Там где проверка не проверяет на ошибку, а влияет на семантику. Например при левом сдвига проверка на 32
[11:09:51] <ada_ru> (I_vlxy_I) https://t.me/adalang/53937
Отсюда
[11:17:30] <ada_ru> (Vadim) А тем временем Ada потихоньку заползает в WASM.
[11:18:38] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Там где проверка не …>
Ясно, нужно будет глянуть, а то упустил как-то такие моменты
[11:19:47] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Ясно, нужно будет гл…>
Не факт что там ещё один такой пример есть. То, что их много - мое предположение. Я Аду то не знаю :-)
[11:19:59] <ada_ru> (I_vlxy_I) отвечает (Vadim) на <А тем временем Ada п…>
Это очень круто!
[11:21:11] <ada_ru> (vasil_sd) отвечает (Vadim) на <А тем временем Ada п…>
Кстати да, киллер-фича: формальная верификация веб-приложений :)
Для интернет-банкинга, например
[11:21:22] <ada_ru> (I_vlxy_I) отвечает (Vadim) на <А тем временем Ada п…>
https://github.com/godunko/adawebpack закинул в дайджест
[11:21:36] <ada_ru> (vasil_sd) Spark/wasm :)
[11:22:17] <ada_ru> (I_vlxy_I) На reddit бы ещё
[11:25:06] <ada_ru> (Vadim) Да погодите, я эту конструкцию только час назад смог на общедоступных кусках собрать.
[11:26:04] <ada_ru> (Vadim) Любой хорошей поделке нужно вылежаться.
[11:32:06] <ada_ru> (Vadim) Кстати, прошел слух, что есть желающие сделать malloc/free для "голого браузера"
[11:32:46] <ada_ru> (Vadim) Если и правда есть - добро пожаловать
[11:35:50] <ada_ru> (I_vlxy_I) отвечает (Vadim) на <Кстати, прошел слух,…>
А у плюсовой либы уворовать не кошерно будет?
[11:36:18] <ada_ru> (I_vlxy_I) Там же даже pthreads уже реализовали
[11:36:19] <ada_ru> (Vadim) Я не знаю ;)
[11:36:44] <ada_ru> (I_vlxy_I) libc есть в полном составе :-) плюс-минус
[11:36:54] <ada_ru> (Vadim) Может кто хочет потренироваться таки в Ada
[11:36:56] <ada_ru> (vasil_sd) отвечает (Vadim) на <Кстати, прошел слух,…>
У меня есть tlsf аллокатор на чистой Аде
[11:37:11] <ada_ru> (vasil_sd) Вчера его откопал, сдул пыть и пытаюсь реанимировать
[11:37:52] <ada_ru> (vasil_sd) Там была попытка всё это формально и на спарке сделать, как починю - выложу на гитхабе :)
[11:39:04] <ada_ru> (vasil_sd) Думаю за пару-тройку дней доделаю до рабочего состояния, но с верификацией пока не бысро будет, там что-то тяжело идёт...
[11:40:04] <ada_ru> (I_vlxy_I) Даёшь рантайм Ады без привязки к libc!
[11:46:24] <ada_ru> (I_vlxy_I) У Go рантайм как раз такой :-)
[11:47:32] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <У Go рантайм как раз…>
Go в этом плане очень грамотно сделан (всё своё) - меньше зависимостей - проще сборка - ниже барьер входа - больше новичков приходят.
[11:48:14] <ada_ru> (vasil_sd) И сразу упор на статичные бинари - то есть распространиение прог без пробелм
[11:49:11] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Go в этом плане очен…>
Ну, у такого подхода есть свои минусы - нужно самостоятельно постоянно следить за тем, как меняются сискаллы у разных осях
[11:49:42] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Ну, у такого подхода…>
Это не сложно и они меняются редко, как правило сохраняя почти полную обратную совместимость...
[11:49:44] <ada_ru> (I_vlxy_I) Ну и портировать сложнее - новая ось, новые сискаллы. А сишная либа она везде стандартная так то
[11:49:56] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <И сразу упор на стат…>
Ага
[11:50:45] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Ну и портировать сло…>
Стандартная, да не совсем. Ньюансов масса и иногда проще написать небольшой новый рантайм, чем продираться через джунгли ньюансов...
[11:51:04] <ada_ru> (I_vlxy_I) Зато от багов и уязвимостей и прочих тараканов смешной либы не зависишь
[11:51:15] <ada_ru> (I_vlxy_I) И весь рантайм легко читать и править
[11:51:34] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <И весь рантайм легко…>
Ага. Мне Ада этим моментом тоже сильно нравится.
[11:52:21] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Ага. Мне Ада этим мо…>
Ну, чтобы его прочитать полностью, адский рантайм, нужно ещё и исходники libc прочитать сейчас
[11:55:33] <ada_ru> (I_vlxy_I) В общем, barelinux runtime для Ады - неплохое упражнение :-)
[11:56:46] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Ну, чтобы его прочит…>
Это линуховый. А металлические рантаймы довольно хорошо читаются
[11:57:46] <ada_ru> (vasil_sd) В линуховом - да, костыли для поддержки pthreads и io через libc на понимаемость влияют...
[11:57:52] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Это линуховый. А мет…>
Ну вот и нужен barelinux :-)
[11:58:10] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <В линуховом - да, ко…>
Дык в виндах тоже такоэ вроде
[11:58:28] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Ну вот и нужен barel…>
Кстати, интересная идея. Только времени много нужно :(
[12:01:30] <ada_ru> (Eugene) barebone runtime -- вот что действительно надо!!!111
[12:01:59] <ada_ru> (vasil_sd) Если наберутся желающие, то я бы поочуствовал. Могу делать аллокаторы памяти и многопоточку с синхронизацией (есть опыт в этом), сеть и прочее - мало опыта.
[12:02:41] <ada_ru> (vasil_sd) Если поднапрячься - то могу даже верифицированные аллокаторы сделать (ну, надеюсь, что осилю :) )
[12:03:17] <ada_ru> (vasil_sd) И промоделировать базовые механизмы синхронизации в многопоточке (есть опыт на TLA+)
[12:04:57] <ada_ru> (vasil_sd) Кстати, TLSF - это hard real-time аллокатор. У него есть гарантия верхняя на время аллокации и деаллокации.
[12:05:24] <ada_ru> (I_vlxy_I) отвечает (Eugene) на <barebone runtime -- …>
Это ж есть
[12:05:31] <ada_ru> (vasil_sd) отвечает (vasil_sd) на <Кстати, TLSF - это h…>
Ну, по модулю кэшей, памяти и прочих железячный вещей
[12:09:17] <ada_ru> (I_vlxy_I) Хардреалтайм в браузере!
[12:09:42] <ada_ru> (I_vlxy_I) Ада для реалтайм игр в браузере :-)
[12:12:56] <ada_ru> (Vadim) barewasm
[12:13:43] <ada_ru> (Vadim) Я вот не горю желанием втянуть сюда ещё и libc
[12:14:02] <ada_ru> (Vadim) Тем более, что толку от неё капля.
[12:14:51] <ada_ru> (vasil_sd) Кстати, основная идея для рил-тайм верифицированного TLSF была - это иметь полностью верифицированные баре-метал проги с динамической аллокацией.
Для полностью верифицированного васма тоже может подойти...
[12:16:06] <ada_ru> (Oleg) отвечает (vasil_sd) на <Ну, по модулю кэшей,…>
Вобще это круто
[12:16:22] <ada_ru> (Oleg) Я бы посмотреть хоьел
[12:16:33] <ada_ru> (Oleg) А для чего он делался?
[12:16:48] <ada_ru> (vasil_sd) отвечает (Oleg) на <А для чего он делалс…>
» Кстати, основная идея для рил-тайм верифицированного TLSF была - это иметь полностью верифицированные баре-метал проги с динамической аллокацией.
[12:17:05] <ada_ru> (vasil_sd) Для железок управления станками
[12:17:20] <ada_ru> (vasil_sd) Когда-то разрабаытвал такое...
[12:17:56] <ada_ru> (Oleg) А что за железо было?
[12:18:35] <ada_ru> (Oleg) И я не понимаю почему "когда то"? почему все интересное кануло в лету?
[12:19:31] <ada_ru> (vasil_sd) отвечает (Oleg) на <А что за железо было…>
Там собственная железка была - плисина + АРМ stm32.
[12:20:04] <ada_ru> (Oleg) Ну а алокатор то под STM32 получается>?
[12:20:06] <ada_ru> (vasil_sd) отвечает (Oleg) на <И я не понимаю почем…>
Ну, экономически нецелесообразно оказалось. Востребованности рынком не было
[12:20:29] <ada_ru> (vasil_sd) отвечает (Oleg) на <Ну а алокатор то под…>
Он универсальный. Ему даёшь кусок памяти и он в нём работает...
[12:21:01] <ada_ru> (Oleg) Я понимаю
[12:21:28] <ada_ru> (Oleg) Интересно просто собрать проест и попробовать, если есть какой то семпл - буду ОЧЕНЬ рад
[12:21:57] <ada_ru> (I_vlxy_I) отвечает (Vadim) на <barewasm>
А потом бэкпортировать на линукс!
[12:22:07] <ada_ru> (vasil_sd) отвечает (Oleg) на <Интересно просто соб…>
Постараюсь в ближайшее время доделать.
Если спать на час меньше, то вроде будет время :)
[12:22:53] <ada_ru> (Oleg) Это да но я думаю...... лучше час поспать 😊 я уже на своем опыте испытал....
[12:22:58] <ada_ru> (vasil_sd) Если интересна теория, то вот: http://www.gii.upv.es/tlsf/files/ecrts04_tlsf.pdf
[12:23:07] <ada_ru> (vasil_sd) Он простой, на самом деле.
[12:23:11] <ada_ru> (Oleg) Спасибо!
[12:23:18] <ada_ru> (vasil_sd) Весь интерес - сделать верифицированным
[12:24:24] <ada_ru> (Oleg) Согласен, хочу чтото типа FreeRTOS но на Ada/SPARK
[12:24:49] <ada_ru> (Oleg) Там нужен, шедулер, менеджер памяти
[12:24:56] <ada_ru> (Oleg) Ну и пока все 😊
[12:25:15] <ada_ru> (vasil_sd) отвечает (Oleg) на <Согласен, хочу чтото…>
Предлагаю глянуть на OpenCOM RTOS. Там формальный дизайн и много идей можно утащить
[12:25:50] <ada_ru> (Oleg) Кстати я вчера анонсировал идею 😊 ну или вброс 😊
[12:25:57] <ada_ru> (Oleg) Рассказываю.......
[12:26:08] <ada_ru> (vasil_sd) отвечает (vasil_sd) на <Предлагаю глянуть на…>
https://books.google.ru/books?id=6_DdAGCMQB4C&pg=PA77&lpg=PA77&dq=opencom+rtos&source=bl&ots=lzmtoqZfHo&sig=ACfU3U1huES23fR-Nss5aoBXtTG4a16iNA&hl=ru&sa=X&ved=2ahUKEwj55eD_oYXnAhVq-yoKHWorDKoQ6AEwC3oECAsQAQ#v=onepage&q=opencom%20rtos&f=false
[12:29:04] <ada_ru> (Oleg) 1. Собираем сообщество профессионалов в написании ПО/Железе/DevOps/Networking
2. При наличии какого то интересного , коммерческого проекта, каждый высказывает свое мнение и готовность/не готовность им заняться частично или полностью.
3. Оговариваем гонорар.
4. Оформляем договор.
5. Сдали - получили деньги.
6. Profit
[12:30:06] <ada_ru> (Oleg) Конкретно сейчас есть туманный проект, но я не могу все делать там один...... пока не понятны финансовые выгоды но шанс есть
[12:31:16] <ada_ru> (vasil_sd) отвечает (Oleg) на <1. Собираем сообщест…>
Я готов участвовать, но только проект должен быть для меня интересен.
Так как зарабатываю стабильно и нормально, просто кодить за деньги неинтересные задачи - это явно не моё.
[12:33:42] <ada_ru> (vasil_sd) отвечает (Oleg) на <1. Собираем сообщест…>
И ещё такой момент. Если проект интересный и там получается что-то интересное сделать, хотелось бы иметь возможность писать по этому поводу статьи небольшие, чтобы популяризовать нормальный подход к разработке железа и софта (как та пара статей на хабре).
[12:34:11] <ada_ru> (Oleg) Да это то не проблема
[12:43:35] <ada_ru> (Лекс) отвечает (I_vlxy_I) на <А потом бэкпортирова…>
Ну и зачем? Васм же сейчас можно гонять на голой оси
[12:44:26] <ada_ru> (vasil_sd) отвечает (Лекс) на <Ну и зачем? Васм же …>
Ну без дополнительной прослойки будет быстрее/надёжнее, я думаю
[12:45:20] <ada_ru> (vasil_sd) отвечает (Oleg) на <Там нужен, шедулер, …>
Кстати, у Ады же есть свои планировщики?
Нужно только дать примитивы для переключения контекстов и синхронизации
[12:45:57] <ada_ru> (Лекс) отвечает (vasil_sd) на <Ну без дополнительно…>
Ради надежности его и притащили) тип песочница и все дела, но есть и транслятор же в нативный код
[12:46:49] <ada_ru> (vasil_sd) отвечает (Лекс) на <Ради надежности его …>
Странно всё это. Если поверх оси, то есть же песочница типа cgroups (докер и пр)
[12:49:01] <ada_ru> (Лекс) Васм машина ещё и универсальная
[12:50:04] <ada_ru> (vasil_sd) отвечает (Лекс) на <Васм машина ещё и ун…>
Да уж. Уже их целый зоопарк, этих виртуальных машин. Одна универсальнее другой :)
[12:50:56] <ada_ru> (vasil_sd) Потом в васм затащат половину функционала явы и будет ещё один большой комбайн.
ява тоже когда-то начиналась как небольшая универсальная ВМ для мелких устройств... :)
[12:51:56] <ada_ru> (vasil_sd) Интересно, почему за основу не взяли llvm машину? бит-код есть, семантика есть...
[12:57:01] <ada_ru> (I_vlxy_I) отвечает (Лекс) на <Ну и зачем? Васм же …>
Чтобы на линухе был нормальный свежий рантайм без зависимостей от libc
[12:57:54] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Интересно, почему за…>
Скорость и компактность. Wasm это ж почти что ast
[12:59:12] <ada_ru> (Лекс) отвечает (vasil_sd) на <Интересно, почему за…>
В браузер? А жирно ли
[13:00:18] <ada_ru> (Лекс) отвечает (I_vlxy_I) на <Чтобы на линухе был …>
Ну и гоняй в васме нормальный свежий рантайм, а линух не нужен 😂
[13:01:48] <ada_ru> (I_vlxy_I) отвечает (Лекс) на <Ну и гоняй в васме н…>
Васм - тормоз. Так то. И многопоточки там нет нормальной
[13:12:38] <ada_ru> (Максим) Вадим Закинуть ссылку в англоязычную группу, или сам закинешь?
[13:13:02] <ada_ru> (I_vlxy_I) На реддит сразу!
[13:16:58] <ada_ru> (Лекс) отвечает (I_vlxy_I) на <Васм - тормоз. Так т…>
ещё молод)
[13:21:07] <ada_ru> (Vadim) Для англообщественности нужно ещё обёртку, бантики, фанфары, шампанское...
[13:24:25] <ada_ru> (I_vlxy_I) отвечает (Vadim) на <Для англообщественно…>
Нефиг! Всё по хардкору!
[13:24:45] <ada_ru> (I_vlxy_I) Release early, release often
[13:27:35] <ada_ru> (Лекс) я думаю, товарищ имел в виду, что в эту жопу без смазки не зайдёт
[13:29:25] <ada_ru> (Vadim) Тут release early во всей красе.
[13:29:44] <ada_ru> (Vadim) Ещё вчера вечером никто повторить не мог.
[13:30:32] <ada_ru> (I_vlxy_I) Кати в прод, а там разберёмся!
[13:42:38] <ada_ru> (Vadim) Открыто открытое тестирование :)
[15:02:32] <ada_ru> (Максим) отвечает (I_vlxy_I) на <Васм - тормоз. Так т…>
Да что там многопоточности, хотя бы исключения завезли! 😂
[15:17:42] <ada_ru> (I_vlxy_I) отвечает (Максим) на <Да что там многопото…>
Ну, исключения для плюсов вполне реализуются. Поддержка от wasn’a тут не обязательна
[15:22:32] <ada_ru> (Oleg) https://github.com/Componolit
[15:22:44] <ada_ru> (Oleg) Хм , нашел интересного много
[15:23:48] <ada_ru> (Oleg) A formally verified XML library in SPARK. Ж-)
[15:23:53] <ada_ru> (vasil_sd) отвечает (Oleg) на <https://github.com/C…>
Очень интересно
[15:24:05] <ada_ru> (Oleg) Мне нужна крипто либрари
[15:24:16] <ada_ru> (Oleg) Конора интересная
[15:24:34] <ada_ru> (Oleg) https://github.com/Componolit/libsparkcrypto
[15:24:45] <ada_ru> (Oleg) Вот это любопытно
[15:28:51] <ada_ru> (Лекс) что она там умеет?
[15:29:05] <ada_ru> (Лекс) и в чём заключается верификация? есть мат модель на каком-нить alloy?
[15:35:59] <ada_ru> (Максим) отвечает (I_vlxy_I) на <Ну, исключения для п…>
Ты знаешь как они вполне реализуются? Через js враппер каждого вызова подпрограммы! 😄
[15:38:36] <ada_ru> (Максим) https://brionv.com/log/2019/10/24/exception-handling-in-emscripten-how-it-works-and-why-its-disabled-by-default/
[15:39:52] <ada_ru> (Oleg) отвечает (Лекс) на <и в чём заключается …>
Я еще не смотрел, мне хоть какая нужна, а не биндинк к какому нибудь жуткому СиМонстру
[15:40:36] <ada_ru> (Oleg) Там парни на аде много чего понаделали я смотрю
[15:41:02] <ada_ru> (Лекс) отвечает (Oleg) на <Я еще не смотрел, мн…>
ток на F* есть tls — можно от туда клацать нужные функции, авторство мелкомягких как по мне так авторитетнее чем никому неизвестной компании
[15:41:22] <ada_ru> (I_vlxy_I) отвечает (Максим) на <https://brionv.com/l…>
В llvm недавно pr был ещё
[15:41:56] <ada_ru> (Лекс) или например на криптоле можно взять, тоже куда авторитетнее, имхо. Я вот не могу доверить крипту своих прилаг криптографии от ноунейма
[15:42:23] <ada_ru> (Oleg) отвечает (Лекс) на <ток на F* есть tls —…>
Мне пока нужен только DES/3DES/AES128 и хэши MD5/SHA1
[15:42:44] <ada_ru> (Oleg) Там ничего сложного (ну по крайней мере AES) но лень писать
[15:43:04] <ada_ru> (Лекс) я просто к вопросу реальной надёжности, оно конечно круто что на спарке, но как насчёт качества и математической корректности
[15:48:52] <ada_ru> (Oleg) Ну вот посмотрю как время будет, что это вообще такое
[15:53:13] <ada_ru> (Максим) MD5/SHA1 есть в GNAT Run-Time Library
[15:55:57] <ada_ru> (vasil_sd) отвечает (Лекс) на <я просто к вопросу р…>
Да, многие путают отсутствие ошибок в ПО и соответствие спекам.
ПО может быть безошибочное, но не соответствовать спекам, могут быть ошибочные спеки и тд
Задача валидации спек формальными методами - отдельная довольно серьёзная задача...
[15:56:54] <ada_ru> (vasil_sd) Свойства заложенные в спеки могут быть некорректными/неполными...
[15:57:26] <ada_ru> (Лекс) Да что уж там, теория чисел не полная =)
[15:58:21] <ada_ru> (Лекс) Я вообще к тому, что сейчас набирает обороты шильдик "верифицированно", но по моему без спек — это просто красивый шильдик в духе "Без ГМО"
[15:58:51] <ada_ru> (vasil_sd) отвечает (Лекс) на <Я вообще к тому, что…>
Именно.
И объяснить это рядовым программерам ой как непросто...
[15:59:36] <ada_ru> (I_vlxy_I) А уж менеджерам...
[16:00:06] <ada_ru> (Лекс) ну а бизнесы нынче вообще всё по барабану
[16:09:56] <ada_ru> (Eugene) как может безошибочное ПО не соответствовать спецификациям? такое ПО может быть и делает что-то полезное, но явно не то, что указано в спеках, а значит оно уже по определению ошибочно
[16:26:12] <ada_ru> (I_vlxy_I) Ошибки в спеке :-)
[16:26:21] <ada_ru> (I_vlxy_I) Это вообще постоянное явление
[16:32:01] <ada_ru> (vasil_sd) отвечает (Eugene) на <как может безошибочн…>
Некоторые под безошибочным понимают "без ошибок времени выполнения".
И считают, что можно взять, например, Хаскель и всё будет хорошо :)
[16:32:59] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Ошибки в спеке :-)>
многие считают, что спеки и требования совсем не нужны :)
Нет спек - нет проблем :)
[16:34:09] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Некоторые под безоши…>
Дык и у Си нет ошибок времени исполнения!
[16:34:16] <ada_ru> (vasil_sd) отвечает (Лекс) на <ну а бизнесу нынче в…>
Ну не совсем, вот амазон, гугл и фейсбук активно занимаются формальными вещами.
Этожжж неспроста :)
[16:34:17] <ada_ru> (I_vlxy_I) Особенно под МК
[16:34:25] <ada_ru> (I_vlxy_I) Да и у асма тоже
[16:34:58] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Да и у асма тоже>
Ага. Ребутнулись по ошибке деления на ноль и дальше работаем :)
[16:35:22] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Ага. Ребутнулись по …>
Ну, оно и не ребутнется же в ряде платформ
[16:35:28] <ada_ru> (I_vlxy_I) Просто хрень будет
[16:35:36] <ada_ru> (I_vlxy_I) И сегфолтов не будет
[16:36:17] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Просто хрень будет>
Ну если хардкорно, то да, можно повырубать все исключения либо iret/retn/тд понаставить в обработчиках
[16:36:43] <ada_ru> (I_vlxy_I) Нет рантайм проверок - нет рантайм ошибок!
[16:37:01] <ada_ru> (I_vlxy_I) С этой точки зрения Си намного безопасней Ады
[16:37:19] <ada_ru> (Oleg) отвечает (I_vlxy_I) на <Нет рантайм проверок…>
В мелких МК только Watchdog кое как поможет
[16:37:32] <ada_ru> (vasil_sd) А от зависаний будем ватч-дог юзать.
Если система недетерминированная и ошибка плавающая, то после NN-го количества ребутов, сомжем-таки отработать какой-то функционал... :)
[16:38:07] <ada_ru> (vasil_sd) То, что при этом какому-то реактору поплохеет, ибо стерженьки передвинуть не успели - ну это фигня :)
[16:38:49] <ada_ru> (Oleg) А еще все теперь на РТОС типа Фри Ртос полезли - а там тоже код такой... странный немного
[16:38:55] <ada_ru> (I_vlxy_I) Вообще, много раз сталкивался с тем, что люди считают сегфолт чем-то плохим.
Но ведь сегфолт - это лучшее, что может случиться с программой у которой внутри ошибка.
[16:39:47] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Вообще, много раз ст…>
Вообще, если бы все ошибки могли быть так вытащены наружу - это была бы сказка. Намного было бы проще жить
[16:41:31] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Вообще, много раз ст…>
Насчёт лучшее - это вопрос дискуссионный. Ибо сегфолт может и не быть фатальным семантически. А нормально его обработать с продолжением работы ПО с места исключения - задача весьма нетривиальная.
[16:42:23] <ada_ru> (vasil_sd) В этом плане мне нравится подход в Лиспе с рестарт-кейсами.
[16:48:14] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Насчёт лучшее - это …>
Чтобы оно было не фатально, нужно специальное проектирование и ещё много разнообразных усилий.
[16:58:11] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Чтобы оно было не фа…>
Это да. Вообще разработка качественного софта требует усилий :)
[17:01:08] <ada_ru> (I_vlxy_I) «А что если UB в коде это не ошибка?» задают иногда такие вот вопросы :-)
[17:03:06] <ada_ru> (I_vlxy_I) Ведь прога не падает и на результаты тестов не влияет :-)
[17:03:42] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <«А что если UB в код…>
Кстати да, сишник и плюсы меня этими уб всегда удивляли. Как можно такое вообще закладывать в стандарт языка?
[17:05:08] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Кстати да, сишник и …>
Можно. Других языках UB просто явным образом не описаны в стандарте. Но они обычно есть.
[17:06:38] <ada_ru> (I_vlxy_I) Что будет в Аде при доступе к объекту который уже удалён и при этом все рантайм проверки отключены?
Что будет при двойном удалении объекта?
[17:07:41] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Что будет в Аде при …>
Это не уб. Тут путаница между языком и результатом компиляции.
[17:08:03] <ada_ru> (I_vlxy_I) Это результат исполнения
[17:08:30] <ada_ru> (I_vlxy_I) В плюсах - это UB, такая ситуация
[17:08:37] <ada_ru> (I_vlxy_I) Это явно прописано
[17:09:10] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Это результат исполн…>
Без сертифицированного компилятора результат может быть любым. А закладывание уб в стандарт языка - это совсем некорректно.
[17:09:46] <ada_ru> (vasil_sd) Язык - это синтаксис + операционная семантика.
Как уб описать в семантике?
[17:11:06] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Язык - это синтаксис…>
Ещё стандартная либа и много чего ещё. Ты просто на язык со своей колокольни смотришь. Это более широкая штука.
[17:12:15] <ada_ru> (I_vlxy_I) Так вот, в описанном мною случае что в Аде, что в ц++ будет UB, только в стандарте с++ про это четко написано, а в стандарте Ады - нет.
[17:12:45] <ada_ru> (vasil_sd) Я смотрю на стандарт языка. И вижу там вещи, которые по определению несовместимы с понятием надёжного и корректного по на этом языке
[17:15:06] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Так вот, в описанном…>
В Аде очень мало случаев, где можно сделать вещи похожие на уб. И то, что уб нет в стандарте - это хорошо. И потенциально опасные вещи вынесены в unchecked*.
[17:15:40] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Я смотрю на стандарт…>
Я понимаю. Но с точки зрения простого программиста хорошо когда в стандарте все возможные варианты UB явно расписаны, и когда о них не замалчивают.
[17:17:43] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Я понимаю. Но с точк…>
Я вот кроме unchecked* не могу сходу придумать, где ещё может быть уб
[17:18:21] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Я вот кроме unchecke…>
Ты в одном месте сделал unchecked_deallocate, и там сработало все хорошо
[17:18:41] <ada_ru> (I_vlxy_I) А в другом месте ты продолжаешь работать с освобождённой памятью
[17:18:55] <ada_ru> (vasil_sd) И обычному программисту aliased и unchecked сразу говорят область возможных проблем
[17:18:57] <ada_ru> (I_vlxy_I) В абсолютно safe модуле
[17:19:14] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <А в другом месте ты …>
Это понятно. А ещё примеры?
[17:19:58] <ada_ru> (vasil_sd) По определению, если используешь unchecked, то уже сам вступаешь на Терра инкогнито
[17:20:09] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Это понятно. А ещё п…>
Выход за границы массива
[17:20:20] <ada_ru> (I_vlxy_I) При отключённых рантайм проверках
[17:20:22] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Выход за границы мас…>
Невозможен.
[17:20:31] <ada_ru> (vasil_sd) Проверки не в языке
[17:20:56] <ada_ru> (I_vlxy_I) Легко. Продемонстрировать на примере проги собранной гнатом?
[17:20:59] <ada_ru> (vasil_sd) Это прагмы - метаязык для компилятора
[17:21:15] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Легко. Продемонстрир…>
Было бы интересно посмотреть
[17:21:36] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Это прагмы - метаязы…>
Без прагм же. Просто -gnatp
[17:22:17] <ada_ru> (vasil_sd) В языке четко написано - выход индекса - исключение. Все ясно и хорошо определено
[17:22:51] <ada_ru> (vasil_sd) Отключение проверок - это опция, которой можно пользоваться а можно нет.
[17:23:17] <ada_ru> (vasil_sd) отвечает (vasil_sd) на <Отключение проверок …>
И это к компилятору, а не к языку
[17:23:38] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Отключение проверок …>
В случае использования этой опции что будет при выходе за границы массива?
[17:23:53] <ada_ru> (I_vlxy_I) Эта опция - часть языка.
[17:24:27] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Эта опция - часть яз…>
Часть метаязыка, а не языковой операционной семантики
[17:26:23] <ada_ru> (vasil_sd) А в сишнике - сложение двух интов это уже уб.
[17:33:36] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Часть метаязыка, а н…>
А про то, что это не язык, а метаязык в стандарте сказано?
[17:33:54] <ada_ru> (I_vlxy_I) Ибо я то открываю стандарт на язык Ада, а там оно.
[17:35:04] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Ибо я то открываю ст…>
Нужно почитать точно, как они определяют прагмы
[17:35:32] <ada_ru> (vasil_sd) Вообще прагмы могут быть и не обязательными
[17:36:50] <ada_ru> (vasil_sd) Более того, в 2012 прагмами оставили именно те, которые можно вообще не поддерживать. А всё языковое в аттрибуты унесли.
[17:37:05] <ada_ru> (vasil_sd) отвечает (vasil_sd) на <Более того, в 2012 п…>
Если мне память не изменяет
[17:38:21] <ada_ru> (I_vlxy_I) Ну, скажем так, с точки зрения программиста результат в Си и Аде тут будет идентичный - хорошее такое, жирное UB.
[17:39:01] <ada_ru> (I_vlxy_I) С точки зрения тех кто работает с формальной верификации, да, Ада сильно лучше.
[17:39:18] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Ну, скажем так, с то…>
Ну, если обобщать, то при несертифицированном компиляторе, любая прога - это UB :)
[17:40:03] <ada_ru> (I_vlxy_I) А сертифицированных у нас и нету :-)
[17:40:08] <ada_ru> (I_vlxy_I) СТРАДАТЬ!
[17:45:53] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <СТРАДАТЬ!>
Есть, compcert :) для сишника :)
[17:47:28] <ada_ru> (vasil_sd) отвечает (vasil_sd) на <Есть, compcert :) дл…>
Они там доопределили UB, выкинули всё сомнительное из стандарта, для остатков определили формально операционную семантику и сделали сертифицированный компилятор
[17:48:24] <ada_ru> (vasil_sd) Жаль, что не Аду/SPARK взяли за основу. Это было бы вообще супер.
[17:59:15] <ada_ru> (Eugene) отвечает (vasil_sd) на <Есть, compcert :) дл…>
"сертифицированный" и "верифицированный" — это совершенно разные понятия.
compcert верифицирован, но про сертификацию я что-то ничего не нашёл.
в то же вермя есть куча всякого сертифицированного ПО, которое явно никто никогда не верифицировал и это просто физически невозможно.
тот же линупс — его некоторые версии сертифицированы всякими ФСТЭКами, но о какой такой формальной верификации там может идти речь?
[18:00:00] <ada_ru> (vasil_sd) отвечает (Eugene) на <"сертифицированный" …>
Ну в данном случае я использовал именно терминологию compcerta и пр.
[18:00:11] <ada_ru> (Eugene) если речь о верифицированных компиляторах, то compcert для подмножества сишечки, и cakeml для подмножества SML
[18:00:15] <ada_ru> (vasil_sd) Сертифицированный не в смысле получен какой-то вертификат
[18:01:03] <ada_ru> (Eugene) отвечает (vasil_sd) на <Ну в данном случае я…>
The CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. By ruling out the possibility of compiler-introduced bugs, verified compilers strengthen the guarantees that can be obtained by applying formal methods to source programs.
The main result of the project is the CompCert C verified compiler, a high-assurance compiler for almost all of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors.
http://compcert.inria.fr
я не вижу тут слова "сертифицированный"
[18:01:52] <ada_ru> (vasil_sd) отвечает (Eugene) на <The CompCert project…>
Там оно даже в названии ..Cert.
[18:03:27] <ada_ru> (vasil_sd) Вот в таком смысле: http://adam.chlipala.net/cpdt/
[18:04:22] <ada_ru> (vasil_sd) А в текстах возможно позаменяли на verified, для понятности
[18:05:20] <ada_ru> (vasil_sd) И вот тут в таком же смысле этот термин применяется: https://coq.inria.fr/
[18:05:45] <ada_ru> (vasil_sd) " Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic),"
[18:06:13] <ada_ru> (vasil_sd) В общем, надеюсь, мне удалось объяснить, какой смысл я вкладывал в "Сертифицированный"
[18:07:00] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Есть, compcert :) дл…>
Есть, но не бывает :-)
[18:08:03] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Есть, но не бывает :…>
Не понял утверждения...
А можно его переформулировать в логике первого порядка, я её чуть лучше понимаю? :)
[18:15:24] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Не понял утверждения…>
Говорят так говорил один (реально неизвестный никому) кореец, который не очень хорошо говорил по русски.
От так отвечал на вопрос «а есть ли у вас там, в корее...» в том случае, когда теоретически это есть и возможно, но на практике не реализуется почти никогда.
[18:16:18] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Говорят так говорил …>
Ну, на практике компцерт есть и работает. И возможно даже где-то используется - нужно посмотреть
[18:17:42] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Ну, на практике комп…>
Это и есть “есть, но не бывает” :-)
Теоретически ты можешь попасть в проект где такой компилятор будет использоваться, но вероятность КРАЙНЕ МАЛА. :-)
[18:22:25] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Это и есть “есть, но…>
Ну с таким подходом, тогда и Ады с ОКамлом не бывает. Это же всё субъективно и относительно.
[18:22:59] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Ну с таким подходом,…>
Они сильно чаще бывают таки. Просто даже если по гитхабу пошариться.
[18:23:36] <ada_ru> (I_vlxy_I) А так да. Особенно Ада - экзотика. Да даже фортран уже экзотика.
[18:23:46] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Они сильно чаще быва…>
Уже перешли к статистике :)
[18:24:51] <ada_ru> (vasil_sd) В общем, есть реальный законченный тулчейн с хорошими верифицированными свойствами. И это реальный факт.
Всё остальное - уже демагогия и пр.
[18:28:18] <ada_ru> (vasil_sd) Кстати, "Who uses compcert": https://www.absint.com/compcert/
[18:28:56] <ada_ru> (vasil_sd) Там AirBus значится в пользователях
[18:31:56] <ada_ru> (vasil_sd) Тут тоже интересно: https://www.absint.com/mtu_fh.htm
[20:25:33] <ada_ru> (Oleg) Да и MTU не хрен собочий
[20:25:42] <ada_ru> (Oleg) Дизеля корабельные делают
[20:25:50] <ada_ru> (Oleg) Ну и электронику к ним
[20:27:54] <ada_ru> (vasil_sd) отвечает (Oleg) на <Дизеля корабельные д…>
Там даже что-то про атомную промышленность мелькало...
[23:03:40] <ada_ru> (Oleg) Собрал три консольные утилиты в один инсталлятор под вашу нелюбимую винду :-) Посмотрим будет ли кто пользоваться :-)
[23:04:02] <ada_ru> (Oleg) Что-то времени катастрофически не хватает , я ещё на работе
[23:35:29] <ada_ru> (Максим) Вот, если вам интересно что в Аде аналогично UB - http://www.ada-auth.org/standards/aarm12_w_tc1/html/AA-1-1-5.html
[23:38:07] <ada_ru> (Максим) Это было еще в Ада 83 http://www.ada-ru.org/arm83/ch01s06.html
[23:42:34] <ada_ru> (I_vlxy_I) отвечает (Максим) на <Вот, если вам интере…>
Erroneous execution видимо?
[23:45:37] <ada_ru> (vasil_sd) Не совсем: 10.c
Saying that something is erroneous is semantically equivalent to saying that the behavior is unspecified. However, “erroneous” has a slightly more disapproving flavor.
[23:45:46] <ada_ru> (vasil_sd) Там дальше ещё идут пояснения
[23:46:04] <ada_ru> (vasil_sd) Implementation Advice: If a bounded error or erroneous execution is detected, Program_Error should be raised.
[23:47:41] <ada_ru> (I_vlxy_I) should а не must btw
[23:47:44] <ada_ru> (vasil_sd) В общем, в яыке есть определение ошибочного поведения как крайний случай недетектированной в рант-тайме ошибки.
[23:47:55] <ada_ru> (I_vlxy_I) "Evaluating a name that denotes a nonexistent object is erroneous." - UB при доступе к удаленному объекту
[23:50:14] <ada_ru> (vasil_sd) Да, до определённой степени. Но такие проблемы чётко очерчены и их постарались изолировать.
Есть большая разница, когда в стандарте написано : если вы сложите два числа и будет переполнение, то сами виноваты, мы умываем руки.
И другое - в крайних случаях, когда мы не можем в принципе сгенерировать проверку, то у вас может быть ошибочное поведение.
[23:51:13] <ada_ru> (vasil_sd) В Аде очень четко расписано когда и что происходит. И только уж совсем крайние случаи - возможность ошибочного поведения.
[23:52:48] <ada_ru> (vasil_sd) И крайние случаи четко прописаны в стандарте и для какой-то части есть ворнинги времени компиляции (типа вот тут ассерт постоянно будет ложным, вот тут у тебя будет ран-тайм ошибка и пр).
[23:53:33] <ada_ru> (I_vlxy_I) ну я ж говорил, что в Аде UB есть? И он таки есть. Но называется по другому. И это очень круто, между прочим!
[23:54:03] <ada_ru> (I_vlxy_I) потому, что если бы не было - значит стандарт написан плохо и не полно.
[23:54:07] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <ну я ж говорил, что …>
Это не совсем UB. Немного другое определение и количество случаев весьма мало
[23:54:24] <ada_ru> (I_vlxy_I) ну, те случаи которые я приводил - они все тут.
[23:54:46] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <ну, те случаи которы…>
Там даже в стандарте написано, что семантически близко, но не одно и то же.
[23:54:48] <ada_ru> (I_vlxy_I) и это совсем UB - программа делает что хочет в этом случае если отключены рантайм проверки.
[23:56:03] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Там даже в стандарте…>
там не используется терминология из языка Си. И там написано не про UB а про unspecified behavior - такой термин в Си есть, и это не UB, то есть этот термин в стандарте Си используется в другом смысле.
[23:56:20] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <и это совсем UB - пр…>
Эх, видимо не получается у меня объяснить принципиальную разницу, когда в языке написано, что складывая чиселки вы можете получить UB и когда написано, что в крайних случаях при работе с Unckecked и пр вы можете получить Errorneous Beh.
[23:57:16] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Эх, видимо не получа…>
я понимаю разницу. в Си на каждый чих ты рискуешь попасть в ситуацию с UB. собственно в С++ (по стандарту) ты не можешь реализовать memcpy не создав UB (это вроде бы будут фиксить).
[23:57:39] <ada_ru> (I_vlxy_I) в Аде UB расположены намного более разумно. но они есть. и это - правильно.
[23:58:14] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <я понимаю разницу. в…>
Ну вот. Как можно с такими языками работать? И тем более что-то надёжное писать? Когда результат даже простейшего факториала - это UB?
[23:58:47] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <в Аде UB расположены…>
Ну ок. Видимо тут вопрос ньюансов терминологии
[23:59:10] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Ну вот. Как можно с …>
только быть вендором компилятора - тогда для тебя эти UB не UB. то есть нужно полностью контроллировать компилятор.