[00:01:18] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <только быть вендором…>
:))) Сколько я ошибок повидал в gcc/clang'e, от неправильной кодогенерации до разной трактовки стандарта плюсов. И UB они тоже по-разному трактуют. Тоже иногда весело бывает
В общем, в плане языкового дизайна Ада даст фору и плюсам и сишке.
[00:02:07] <ada_ru> (I_vlxy_I) ну, сишный компилятор возможно вылизать до адекватного состояния. плюсовый - нет. Можно ли адский - не знаю. GNAT вот периодически падает таки.
[00:07:34] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <ну, сишный компилято…>
Полностью вылизать компилятор C99 невозможно (ИМХО), именно из-за особенностей стандарта языка (не думаю что реально сделать операционную семантику для 100% стандарта). ComCert поддержали практически максимум из того, что реально поддержать для надёжного компилятора.
Плюсы точно нереально в обозримом будущем. И мне не понятен бизнес, который так лелеит плюсы. Намного разумнее использовать другие языки почти в любых задачах, будет дешевле сопровождать и развивать проекты.
GNAT - думаю можно постепенно расширяя подмножество спарка и переводя компилятор на спарк, довести до хорошего состояния. Можно ли для 100% Ады сделать формальную операционную семантику - не знаю, но шансы хорошие.
[00:08:33] <ada_ru> (I_vlxy_I) плюсы - скорость! за, сравнительно, небольшие деньги.
[00:09:15] <ada_ru> (I_vlxy_I) с этим безусловно можно поспорить. но я опять не представляю как тут выяснить верно утверждение или ложно 🙂 как поставить эксперимент
[00:09:38] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <плюсы - скорость! за…>
Ну та же Ада во многих задачах даст сопоставимую скорость при выключенных проверках.
На мой взгляд оптимум - control flow - Ada, high performance data flow - С.
[00:10:47] <ada_ru> (vasil_sd) Обоснование простое: data flow - регулярный, легко вычистить ошибки на тестах, control flow - не требует хай-перворманса и можно верифицировать
[00:11:15] <ada_ru> (I_vlxy_I) ну, когда я пробовал, на Аде у меня не вышло сопоставимую скорость получить. сильно подкачала стандартная библиотека Ады.
в реальных же задачах будут именно стандартной либой пользоваться а не пилить всё с самого основания.
[00:12:04] <ada_ru> (I_vlxy_I) а на расте решение уступало плюсовому вроде бы процентов на 20
[00:12:07] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <ну, когда я пробовал…>
У меня опыт на Аде сравнительно небольшой и стандартной библиотекой я не пользовался практически, поэтому тут совсем нет опыта и нет мнения
[00:12:33] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <а на расте решение у…>
Раст да, очень многообещающий язык
[00:12:57] <ada_ru> (vasil_sd) У него хорошие шансы дать надёжность Ады при производительности сишника/плюсов
[00:13:18] <ada_ru> (I_vlxy_I) ну вот когда берут проект и пишут - пользуются стандартной либой и еще 100500 библиотек. и от качества либ, от качества инструментария (компилятора, отладчиков, и даже IDE) очень сильно зависит и скорость разработки и качество кода и скорость кода
[00:13:19] <ada_ru> (vasil_sd) Правда синтаксис у него - ужас ужасный
[00:13:54] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <ну вот когда берут п…>
Я больше по системному программированию, тут не так часто стандартные либы используют :)
[00:13:58] <ada_ru> (I_vlxy_I) язык безусловно важен, но так себе качество всего остального может перевесить в проектах где много разнородных разработчиков работает и сжатые сроки
[00:14:29] <ada_ru> (I_vlxy_I) ладно, я офф на минут 40
[00:14:49] <ada_ru> (vasil_sd) А я спать :)
[00:15:58] <ada_ru> (I_vlxy_I) good night 🙂
[00:16:17] <ada_ru> (vasil_sd) thanks :)
[03:06:00] <ada_ru> (Oleg) А я вот мать его только с работы домой еду
[03:06:13] <ada_ru> (Oleg) А завтра к максимум 10
[11:48:56] <ada_ru> (vasil_sd) Максим , а вы случаем не в курсе, GnatProve тоже на lal перевели?
А то пытаюсь реанимировать TLSF аллокатор на спарке, а он даже нормально проверку запустить на может, пишет, что не находит тела Ghost процедур (я их для аскиоматизации битовых операций использую). Тот же самый код в GNAT2016 нормально проверялся (там не всё было доказано, но по крайней мере процесс проверки проходил до конца, безо всяких "missing body"
[13:07:16] <ada_ru> (Максим) отвечает (vasil_sd) на <Максим , а вы случае…>
Кажется не переводили
[13:09:50] <ada_ru> (vasil_sd) отвечает (Максим) на <Кажется не переводил…>
В общем сейчас всё сильно изменилось, пытаюсь на spark-by-example понять что же поменялось и те примеры, что оттуда пробовал, не проходят проверки :(
И ограничения времени для пруверов увеличивал и пр - никак...
В общем, ощущение, что всё стало ещё сырее и нестабильнее чем 3-4 года назад :(
[13:19:23] <ada_ru> (Nikita) 👌Доброе утро, уже подписали в нашу закрытую группу ?
[13:53:17] <ada_ru> (vasil_sd) отвечает (vasil_sd) на <В общем сейчас всё с…>
В общем не всё так плохо, как показалось на первый взгляд. Но пример с битовыми векторами целиком верифицировать так и не удалось. Несколько vc никак не хотят прувиться, нужно будет во внутренности лезть и смотреть :(
[13:54:44] <ada_ru> (vasil_sd) Введение аксиоматики теперь не так как раньше, нужно почти всё битовое в tlsf менять...
[15:28:33] <ada_ru> (I_vlxy_I) Работают люди :-) инструмент развивается
[15:30:54] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Работают люди :-) ин…>
Да, видимо быстро развивается
Сейчас посмотрел SPARK lemma library - там половина того, что мне нужно было когда-то уже есть. Это радует :)
[15:40:59] <ada_ru> (Eugene) леммы, значит, говорите.... этак спарк скоро догонит кока...
[16:54:11] <ada_ru> (vasil_sd) отвечает (Eugene) на <леммы, значит, говор…>
Нее, спарк не будет заменой коку. Спарк/gnatporve - это логика первого порядка, и он использует кок для ручного доказательства некоторых утверждений, когда смт солверы не справились.
кок - это эквивалент логикам высшего порядка, только в зависимых типах, спарку туда не нужно :)
[18:32:11] <ada_ru> (vasil_sd) Перекладываю TLSF на новый GnatProve и могу сказать, что прогресс тулов очень существенный. Особенно порадовала консоль ручного доказательства, намного проще, чем когда-то через Coq. Всё еще выглядит довольно сыроватым и юзабилити хромает, но видно, что экосистема спарка развивается сильно и быстро.
Когда полноценно завезут сепарационную логику и указатели - это будет самый продвинутый инструментарий в мире для верификации ПО в промышленных масштабах.
Ещё бы компилятор SparkCert и была бы сказка :)
В общем, я впечатлён :)
[18:34:32] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Перекладываю TLSF на…>
Дык у них заказчики очень крутые :-) та же Nvidia
[18:35:11] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Дык у них заказчики …>
Ага. Наконец-то верификация начала выходить за пределы аэроспейса
[18:35:30] <ada_ru> (vasil_sd) В смысле серьёзно, промышленно выходить
[18:36:08] <ada_ru> (Eugene) отвечает (vasil_sd) на <В смысле серьёзно, п…>
seL4 уже 10 лет как существует, а прямо что бы захватила мир — до сих пор и не слышно
[18:36:54] <ada_ru> (vasil_sd) отвечает (Eugene) на <seL4 уже 10 лет как …>
Она очень специфичная и нишевая. И там очень сложная поддержка и развитие. То есть в широкие массы тяжело идти с таким багажом
[18:37:19] <ada_ru> (vasil_sd) А тулы вокруг спарка сейчас уже готовы для уровня продвинутого программиста
[18:37:51] <ada_ru> (vasil_sd) Скоро будут готовы для уровня среднего программиста с несильным знанием матлогики и computer science
[18:47:36] <ada_ru> (I_vlxy_I) Даёшь дрова на спарке!
[18:47:59] <ada_ru> (I_vlxy_I) И фирмварезы
[18:48:51] <ada_ru> (mister_alexander) Дрова не нужны
[18:49:04] <ada_ru> (mister_alexander) Без них все работать должно
[18:56:30] <ada_ru> (I_vlxy_I) отвечает (mister_alexander) на <Дрова не нужны>
Дрова сразу в самой железке должны быть?
[18:57:25] <ada_ru> (shiz01) отвечает (I_vlxy_I) на <Дрова сразу в самой …>
Доп уровень абстракции и заявка на модульность, не зависимую от работчего окружения?
Интересно.
[18:58:24] <ada_ru> (mister_alexander) отвечает (I_vlxy_I) на <Дрова сразу в самой …>
Конечно
[19:00:46] <ada_ru> (I_vlxy_I) отвечает (shiz01) на <Доп уровень абстракц…>
Так уже было. В древние времена у яблока
[21:05:42] <ada_ru> (Максим) @vasil_sd А ты не вкурсе, случайно, как доказывается корректность lockfree алгоритмов?
[21:14:03] <ada_ru> (vasil_sd) отвечает (Максим) на <@vasil_sd А ты не вк…>
Некоторые способы знаю, но серьезно этим не занимался.
[21:14:52] <ada_ru> (vasil_sd) Там моделчекинг и его разновидности используются.
[21:15:29] <ada_ru> (vasil_sd) Из моего опыта, я только доказывал свойства интринсиков
[21:16:40] <ada_ru> (vasil_sd) И ещё доказывал свойства алгоритма рандеву для многоядерной архитектуры проца
[21:22:04] <ada_ru> (vasil_sd) Какая-то версия рандеву у меня тут выложена: https://github.com/vasil-sd/rendezvous-protocol
[21:37:04] <ada_ru> (vasil_sd) отвечает (vasil_sd) на <Какая-то версия ранд…>
Там спека немного кривовата, сейчас посмотрел, видимо, там довольно древний вариант. Но он должен быть рабочим.
[21:38:03] <ada_ru> (vasil_sd) отвечает (vasil_sd) на <Там спека немного кр…>
В смысле спека тоже должна быть вполне рабочей. Её можно моделировать и проверять свойства.
[22:32:21] <ada_ru> (I_vlxy_I) https://annexi-strayline.com
Адакод на скриншотах!
[22:35:31] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <https://annexi-stray…>
Ну в той области, альтернатив-то по сути нет.
[22:38:02] <ada_ru> (I_vlxy_I) Спарку - наверно
[22:38:37] <ada_ru> (I_vlxy_I) Но Ада не выглядит сильно надёжней всего остального
[22:39:40] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Но Ада не выглядит с…>
Почему? Как язык вполне себе хорошо задизайнена с прицелом на надёжность.
[22:40:17] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Почему? Как язык впо…>
Слишком мало проверяет на этапе компиляции, слишком много в рантайме
[22:46:09] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Слишком мало проверя…>
Проверяет почти максимум того, что можно проверить не переходя к серьёзному формальному анализу
[22:46:34] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Проверяет почти макс…>
Ты точно про Аду а не Спарк?
[22:46:35] <ada_ru> (vasil_sd) Нужно серьезнее компилятора - есть анализаторы
[22:46:46] <ada_ru> (vasil_sd) Точно про Аду
[22:47:06] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Точно про Аду>
В Аде забытый return значения из функции это не ошибка
[22:47:16] <ada_ru> (I_vlxy_I) Максимум будет варнинг
[22:47:46] <ada_ru> (I_vlxy_I) Найди ещё такой язык (кроме с++, где тоже тут все плохо)
[22:49:15] <ada_ru> (t91x0) отвечает (I_vlxy_I) на <Найди ещё такой язык…>
Borland Pascal, поди.
Хотя я не помню уже.
[22:49:42] <ada_ru> (t91x0) Про perl, php и python сказать не могу.
[22:49:46] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <В Аде забытый return…>
Хм.. Сейчас проверю
[22:49:56] <ada_ru> (I_vlxy_I) отвечает (t91x0) на <Про perl, php и pyth…>
Там нет этапа компиляции :-)
[22:50:18] <ada_ru> (t91x0) отвечает (I_vlxy_I) на <Там нет этапа компил…>
Ну можно ведь получить ошибку запуска скрипта
[22:50:31] <ada_ru> (t91x0) И файлы .pyc в питоне есть
[22:51:16] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <В Аде забытый return…>
main.adb:18:04: missing "return" statement in function body
main.adb:20:03: statement expected
gprbuild: *** compilation phase failed
Ругается и не компилит. В чём проблема?
[22:51:27] <ada_ru> (I_vlxy_I) Ещё штука которую современные ЯП не пропускают в compile time (даже с++, если std::variant) https://t.me/adalang/57195
[22:51:35] <ada_ru> (t91x0) отвечает (vasil_sd) на <main.adb:18:04: miss…>
А вы режим ада-83 включите
[22:51:51] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <main.adb:18:04: miss…>
А ты if..else добавь
[22:51:58] <ada_ru> (vasil_sd) отвечает (t91x0) на <А вы режим ада-83 вк…>
Ну, давайте тогда и сравнивать с языками 83-го года
[22:52:16] <ada_ru> (I_vlxy_I) То есть чтобы в одной из веток было забыто
[22:53:11] <ada_ru> (vasil_sd) main.adb:21:10: "return" statement missing following this statement
main.adb:21:10: Program_Error might have been raised at run time
gprbuild: *** compilation phase failed
[22:53:32] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <main.adb:21:10: "ret…>
Именно. Не ошибка. Предупреждение
[22:53:35] <ada_ru> (vasil_sd) Ну и это мы уже обсуждаем реализации компиляторов, а не язык
[22:53:40] <ada_ru> (I_vlxy_I) Язык не требует ошибки тут
[22:53:55] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Именно. Не ошибка. П…>
Ну не знаю. Не компилится ведь?
[22:54:26] <ada_ru> (I_vlxy_I) До компа доберусь, пример нарою
[22:54:47] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Язык не требует ошиб…>
Язык и не может требовать проводить анализ на достижимость и пр.
[22:55:03] <ada_ru> (Oleg) Сейчас все скажут «а вот раст .....» :-)
[22:55:24] <ada_ru> (vasil_sd) отвечает (Oleg) на <Сейчас все скажут «а…>
У раста свои приколы
[22:56:02] <ada_ru> (vasil_sd) В Аде сделали программирование максимально безопасным, до границы уже необходимости серьёзных анализаторов кода.
[22:56:04] <ada_ru> (t91x0) отвечает (vasil_sd) на <Язык и не может треб…>
А вот C# требует
[22:56:48] <ada_ru> (vasil_sd) отвечает (t91x0) на <А вот C# требует>
Возможно, я последний раз его лет 15 назад видел, когда писал на нём мелкую игрушку под вин-мобайл...
[22:57:47] <ada_ru> (vasil_sd) На мой взгляд - Ада один из очень немногих языков, который очень хорошо определён, как язык и хорошо продуман.
[22:58:29] <ada_ru> (vasil_sd) Лучше - уже только что-то из ML'ей и подобных, которые с самого начала дизайнились практически формально
[22:59:36] <ada_ru> (t91x0) отвечает (vasil_sd) на <Лучше - уже только ч…>
Приходите к нам в rust_offtopic
[22:59:57] <ada_ru> (vasil_sd) отвечает (t91x0) на <Приходите к нам в @r…>
Для раста есть формальная операционная семантика?
[23:00:10] <ada_ru> (t91x0) отвечает (vasil_sd) на <Для раста есть форма…>
Вот там и спросите. Я сомневаюсь.
[23:01:04] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Язык и не может треб…>
Проверь вообще в любом другом языке - java, swift , kotlin, rust, go
[23:01:05] <ada_ru> (I_vlxy_I) C#
[23:01:10] <ada_ru> (vasil_sd) отвечает (t91x0) на <Вот там и спросите. …>
Если нет, то тогда пока малоинтересно. За всеми языками следить - это много времени нужно
[23:02:18] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Проверь вообще в люб…>
Ок. Не спорю, что средства анализа хорошо развились и возможно минимальные требования по анализу начали и в стандарты языков затаскивать.
Давайте тогда Аду с Codepeer рассматривать?
[23:03:01] <ada_ru> (vasil_sd) Или спарк + гнатпрув. Чего уж мелочиться :)
[23:03:38] <ada_ru> (vasil_sd) В каких языках ещё контракты в стандарте? Раз-два и обчелся.
А аналоги гнатпрува?
[23:03:58] <ada_ru> (vasil_sd) А ещё чтобы и промышленный язык был
[23:04:38] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <В каких языках ещё к…>
Я про то, что сейчас есть под руками у массового программиста. Ада без стероидов уже не является чем-то выдающимся в плане надежности. Ада - хорошо тут, но не отлично.
[23:05:01] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Я про то, что сейчас…>
Да ладно, даже без стероидов. - Предикаты на типы
[23:05:16] <ada_ru> (vasil_sd) Контракты даже без стероидов работают
[23:05:30] <ada_ru> (I_vlxy_I) А codepeer сильно отдельных денег и административных усилий требует
[23:05:31] <ada_ru> (vasil_sd) Да, рантайм, но у других и такого нет
[23:05:46] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Контракты даже без с…>
Контракты даже в шарпе есть
[23:06:05] <ada_ru> (I_vlxy_I) И скоро будут в плюсах
[23:06:25] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Контракты даже в шар…>
Возможно, повторюсь, что не слежу за всеми языками, ибо много их развелось
[23:06:38] <ada_ru> (Oleg) Шарп на самом деле неплохой язык
[23:06:49] <ada_ru> (Oleg) Но я на него забил
[23:06:52] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Контракты даже в шар…>
Но в Аде они одни из первых появились и были нормально поддержаны
[23:07:18] <ada_ru> (vasil_sd) отвечает (Oleg) на <Шарп на самом деле н…>
Для быстропроганья UI - вобще замечательным показался 15 лет назад
[23:07:30] <ada_ru> (Oleg) Все фигня , Ада няшная :-)
[23:07:41] <ada_ru> (vasil_sd) отвечает (Oleg) на <Все фигня , Ада няшн…>
👍
[23:09:04] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Но в Аде они одни из…>
Раньше в Эйфеле были вроде
[23:09:15] <ada_ru> (vasil_sd) У меня любимые языки - это OCaml и Ада.
А пишу больше всего на плюсах 😩
[23:09:22] <ada_ru> (I_vlxy_I) Или там только инварианты?
[23:09:37] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Раньше в Эйфеле были…>
Я думаю и эйфель здесь не первопроходец
[23:10:01] <ada_ru> (vasil_sd) Из промышленных - Ада думаю одна из первых, или вообше первая
[23:10:30] <ada_ru> (vasil_sd) Идеи контрактов идут ещё со времён Дейкстры и Гриса
[23:10:53] <ada_ru> (vasil_sd) Книжка такая была "Наука программирования" у Гриса
[23:11:28] <ada_ru> (vasil_sd) А первоначально такой тип анализа императивных прог - Тони, наше всё, Хоар
[23:11:51] <ada_ru> (vasil_sd) Так что, контракты - это очень и очень старое
[23:13:03] <ada_ru> (I_vlxy_I) Эйфель вроде именно как промасленный позиционируется
[23:13:23] <ada_ru> (I_vlxy_I) Высоконадежный за много денег
[23:13:46] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Эйфель вроде именно …>
Не слышал о множестве success story с его участием. Может где-то и используется, но что-то не видно и не слышно
[23:15:44] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Не слышал о множеств…>
Есть, но не бывает? :-)
[23:16:07] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Есть, но не бывает? …>
:))
Я этого не говорил :))
[23:16:27] <ada_ru> (vasil_sd) Сейчас интесно стало, ищу, где он испольуется
[23:19:29] <ada_ru> (vasil_sd) Вот нашёл немного: https://www.eiffel.com/company/customers/
[23:19:49] <ada_ru> (vasil_sd) Даже боинг там есть. Интересно, для чего его в боинге применяют?
[23:20:59] <ada_ru> (Oleg) отвечает (vasil_sd) на <Даже боинг там есть.…>
737 MAX ? :-)
[23:21:30] <ada_ru> (vasil_sd) :))))
да, тож такая мысль мелькнула, но над трагедией как-то нехорошо смеяться
[23:21:58] <ada_ru> (vasil_sd) 737 MAX - это общеамериканская трагедия :)
[23:22:40] <ada_ru> (vasil_sd) Вот тут интересно эйфель рекламируют: https://www.eiffel.com/values/model-driven-development/
[23:23:11] <ada_ru> (Oleg) Да людей жаль - компания должна понести ответственность
[23:23:29] <ada_ru> (vasil_sd) отвечает (Oleg) на <Да людей жаль - комп…>
Они уже и так несут, пока только финансовую
[23:24:19] <ada_ru> (vasil_sd) отвечает (vasil_sd) на <Вот тут интересно эй…>
Напомнило Event-B и Atelier-B подход. Но Atelier-B там всё по-взрослому, формально с солверами
[23:26:46] <ada_ru> (I_vlxy_I) посольку Eiffel в свое время DoD не проталкивал в соответствующие отрасли, ему приходится туда проникать "по любви" 🙂
[23:27:37] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <посольку Eiffel в св…>
Вот думаю скачать, посмотреть, какая там экосистема.
Сам язык не сильно нравится, через чур уж минималистичностью увлеклись
[23:27:47] <ada_ru> (vasil_sd) В смысле синтаксис языка
[23:27:54] <ada_ru> (t91x0) Теоретически Eiffel должен применяться в каком-нибудь бывшем Sagem и прочих европейских оборонных конторах
[23:27:59] <ada_ru> (I_vlxy_I) ну, не сказать чтобы он прям таки минималистичен 🙂 а IDE там норм.
[23:28:09] <ada_ru> (I_vlxy_I) и с пачкой стандартных либ идет в комплекте - и сеть и гуй
[23:28:30] <ada_ru> (I_vlxy_I) солверов и консоли для доказательства корректности я там не помню 🙂
[23:28:33] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <ну, не сказать чтобы…>
По сравнению с Адой он какой-то не сильно читаемый
[23:28:53] <ada_ru> (I_vlxy_I) но что касается обмазивания рантайм проверками всевозможными всего подряд - там этого есть более чем
[23:29:05] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <солверов и консоли д…>
Мне интересно, как они поддержали modeling workflow
[23:29:44] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <По сравнению с Адой …>
ну, тут уже на вкус и цвет... кому то и ада не читабельная, а кому-то и с++.
[23:30:28] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <ну, тут уже на вкус …>
Да ну. Ада по-моему, даже не видевшими её программерами сносно читается, ибо одна из целей языка была такая
[23:31:09] <ada_ru> (Oleg) С Perl никто не сравнится
[23:31:12] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Да ну. Ада по-моему,…>
ну, если язык не то чтобы многословный, а многострочечный - что толку, если ты легко прочитал то, что на экране, если на экране почти ничего и не поместилось?
[23:31:22] <ada_ru> (I_vlxy_I) листание исходников - это сильно дорогая операция
[23:32:01] <ada_ru> (t91x0) отвечает (vasil_sd) на <По сравнению с Адой …>
Есть несколько культур, я не знаю, как точнее назвать. Английская, французская, немецкая.
Что сделали с немецкой, всем известно. Французскую тоже изрядно задавили, эйфель как раз из неё. А наиболее привычна вам и мне - английская.
[23:32:05] <ada_ru> (vasil_sd) А плюсы - да, вырвиглазный синтаксис. Всё жду, когда они наконец перестанут стесняться и завезут юникодные скобочки в язык :) В юникоде есть даже горизонтальные :)
[23:32:58] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <А плюсы - да, вырвиг…>
надо эмоджи в язык добавить.💩
[23:33:29] <ada_ru> (Oleg) отвечает (I_vlxy_I) на <надо эмоджи в язык д…>
В питон :-)
[23:33:31] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <надо эмоджи в язык д…>
точно !
Это отличная идея и может выстрелить по вирусному принципу :)
[23:34:34] <ada_ru> (vasil_sd) отвечает (Oleg) на <В питон :-)>
Питон и так популярен, ему эмоджи не нужны :)
[23:37:10] <ada_ru> (Oleg) отвечает (vasil_sd) на <Питон и так популяре…>
Мне кажется ему недолго осталось
[23:37:18] <ada_ru> (Oleg) Ещё лет 20 :-)
[23:37:31] <ada_ru> (vasil_sd) отвечает (Oleg) на <Ещё лет 20 :-)>
до версии 4.0
[23:38:11] <ada_ru> (Oleg) отвечает (vasil_sd) на <до версии 4.0>
Когда они опять все сломают
[23:38:24] <ada_ru> (vasil_sd) Питон занял хорошую нишу и выковыривать его оттуда другим языкам будет тяжело.
Даже JS'у
[23:38:38] <ada_ru> (Oleg) И с 3 на 4 не перейти просто так
[23:39:01] <ada_ru> (vasil_sd) отвечает (Oleg) на <И с 3 на 4 не перейт…>
Ну конечно, иначе будут традиции нарушены :)
[23:40:02] <ada_ru> (Oleg) Причём если компилируемые языки хрен с ними, исполняемый файл будет работать, то тут надо ставить интерпретатор нужный
[23:40:30] <ada_ru> (I_vlxy_I) питон можно и в ехешник собрать
[23:40:31] <ada_ru> (I_vlxy_I) так то
[23:41:28] <ada_ru> (Oleg) отвечает (I_vlxy_I) на <питон можно и в ехеш…>
Да но это немного странно
[23:41:31] <ada_ru> (vasil_sd) отвечает (Oleg) на <Причём если компилир…>
С бинарями тоже не всё так гладко. ld-linux.so другой версии или glibc - танцы с бубном обеспечены, даже если пропатчить в бинаре пути загрузки и положить в нужные места старые либы
[23:41:44] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <питон можно и в ехеш…>
Там весьма условный exeшник
[23:42:00] <ada_ru> (vasil_sd) А если cython - то это какбы не совсем питон уже
[23:43:30] <ada_ru> (Oleg) Собрал кстати исполняемый файл на Go под suse , а на CentOS он выпал в ошибку
[23:43:43] <ada_ru> (vasil_sd) отвечает (Oleg) на <Собрал кстати исполн…>
ldd что говорит?
[23:43:53] <ada_ru> (Oleg) Пока не смотрел
[23:44:04] <ada_ru> (Oleg) Завтра погляжу
[23:44:46] <ada_ru> (vasil_sd) вероятнее всего версии каких-то либ не те приехали.
Там же наверняка что-то цеплялось через FFI
[23:45:41] <ada_ru> (Oleg) Поковыряюсь
[23:46:50] <ada_ru> (vasil_sd) Кстати, если даже ldd ничего не скажет, это не означает, что он либы не тянет. Ибо что-то может тянуть и через явный dlopen
[23:47:23] <ada_ru> (vasil_sd) Ещё нужно strace'ом глянуть, что он там от системы хочет.
[23:47:58] <ada_ru> (Oleg) Ага
[23:49:32] <ada_ru> (vasil_sd) Я тут как-то пытался сборку postgres сделать, чтобы под многими системами работало (нужно для тестов было), так с этими бинарями и либами так замучался, ужос
[23:49:46] <ada_ru> (I_vlxy_I) мне кажется, или gnat дюже тупой? https://godbolt.org/z/pKWZJM
[23:50:14] <ada_ru> (I_vlxy_I) example.adb:5:05: warning: "return" statement missing following this statement
example.adb:5:05: warning: Program_Error may be raised at run time
Compiler returned: 0
[23:50:57] <ada_ru> (vasil_sd) Тут нужен SMT солвер, чтобы такие вещи решать
[23:51:14] <ada_ru> (vasil_sd) Видимо на частные случаи такого анализа просто забили
[23:51:39] <ada_ru> (I_vlxy_I) мне кажется, что такой "солвер" в компиляторе вообще любого языка есть
[23:51:52] <ada_ru> (I_vlxy_I) если не брать в рассчет фортран и с++
[23:51:57] <ada_ru> (vasil_sd) В общем виде по-умолчанию нет
[23:52:02] <ada_ru> (vasil_sd) Ибо дорого
[23:52:46] <ada_ru> (vasil_sd) Это же решение довольно сложной логической задачи, доказать, что случаи в ветках покрывают все варианты
[23:53:20] <ada_ru> (vasil_sd) И она вобще неразрешима, насколько я помню (тут от языка зависит, какие он выражения допускает)
[23:53:52] <ada_ru> (I_vlxy_I) погоди, компиляторы современные же делают escape analysis, тут не нужны все пути, тут довольно узкая штука
[23:55:16] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <погоди, компиляторы …>
В смысле пути? Тут есть предикаты на ветках и нужно доказать, что эти предикаты охватывают все варианты. А предикаты могут быть сколь-угодно сложные.
[23:56:02] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <В смысле пути? Тут е…>
достаточно доказать, что они не охватывают все варианты 🙂 то есть найти один (ЛЮБОЙ!) вариант который проскочет
[23:56:16] <ada_ru> (vasil_sd) То есть, в базовом варианте можно сделать ап-лифтинг и всё сплющить к одному уровню, но потом начинается жесть
[23:56:55] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <достаточно доказать,…>
Ага, найти контр-пример. Тоже такая себе задача, дуальная к satisfiability
[23:57:52] <ada_ru> (vasil_sd) Хотя, я не компиляторщик, может там что и интересное уже придумали
[23:59:18] <ada_ru> (I_vlxy_I) я поэкспериментировал - gnat тут не тупой. он скорее добрый чем тупой 🙂 остальные компиляторы, что я попробовал, выдают просто ошибку компиляции
[23:59:26] <ada_ru> (I_vlxy_I) ибо нефиг, ибо безопасность прежде всего 🙂
[23:59:31] <ada_ru> (I_vlxy_I) А Ада - добрая дама.