[00:39:38] <ada_ru> (vasil_sd) Сейчас GPS опять упал :( уже раз пятый за день :(
В связи с этим вопрос: а кто какие IDE использует для Ады? (VIM, Emacs хороши, но всё-таки хочется что-нибудь более приближеное к GPS)
GPS почти всем устраивает, кроме стабильности...
[00:43:32] <ada_ru> (Maxim Reznik) А у вас есть Си файлы в проекте?
[00:43:53] <ada_ru> (vasil_sd) отвечает на <(Maxim Reznik) А у …>
Нет, только Ада
[00:44:53] <ada_ru> (vasil_sd) Имеет смысл попробовать настроить vscode с плагинами? Хорошая альтернатива GPS? или нет?
[00:45:46] <ada_ru> (Лекс) Если нравится "молодёжное стильное" и переодические баги поведения интерфейса, лежащие вне посягаемости логики
[00:46:08] <ada_ru> (Максим) Попробовать то можно, но меня на долго не хватило, слишком привык к жпс
[00:46:49] <ada_ru> (vasil_sd) отвечает (Лекс) на <Если нравится "молод…>
Ну, если не сильно далеко вне логики, то может и не страшно будет :)
А по функционалу как?
[00:47:22] <ada_ru> (vasil_sd) отвечает (Максим) на <Попробовать то можно…>
А по функционалу как, по сравнению с GPS?
Кстати, у вас GPS стабильно работает?
[00:47:43] <ada_ru> (Максим) Там может даже отладчик лучше 🙃
[00:47:46] <ada_ru> (Лекс) отвечает (vasil_sd) на <Ну, если не сильно д…>
Я не для Ады юзаю.
У меня частенько бывают баги с вводом/буфером, но возможно это из-за того что у меня железо не новое
[00:48:12] <ada_ru> (Лекс) s/баги/лаги
[00:48:39] <ada_ru> (vasil_sd) отвечает (Лекс) на <Я не для Ады юзаю.
…>
Понятно. Меня в первую очередь Ада-специфичное интересует, интеграция с тулами, в частности Gnatprove....
[00:48:41] <ada_ru> (Лекс) хотя с буффером и баги бывают)
[00:48:56] <ada_ru> (vasil_sd) отвечает (Максим) на <Там может даже отлад…>
А gnatprove прикручен нормально?
[00:49:08] <ada_ru> (Максим) отвечает (vasil_sd) на <А по функционалу как…>
Да более менее, но я не на gnat community 2019 сижу
[00:49:23] <ada_ru> (vasil_sd) отвечает (Максим) на <Да более менее, но я…>
А на каком?
[00:50:41] <ada_ru> (Максим) отвечает (vasil_sd) на <А gnatprove прикруче…>
Нет, это не прикручивали вообще. А что там нужно? Просто запускать и отображать диагностику? Тогда это просто
[00:51:16] <ada_ru> (vasil_sd) отвечает (Максим) на <Нет, это не прикручи…>
Мне очень удобна ещё расцветка, это доказал, это доказал, здесь обломался...
[00:51:26] <ada_ru> (Максим) отвечает (vasil_sd) на <А на каком?>
Или на самом распоследнем или на каком-то из релизов, когда как
[00:53:24] <ada_ru> (vasil_sd) отвечает (Максим) на <Или на самом распосл…>
А вы случаем не в курсе, какой порядок цен может быть на Pro версию, если я захочу как индивидуальный разработчик с ней поиграться?
Есть желание посмотреть на всю доступную экосистему от adacore
[00:54:21] <ada_ru> (Максим) Нет, я совсем не в теме цен.
[00:55:04] <ada_ru> (vasil_sd) отвечает (Максим) на <Нет, я совсем не в т…>
Ясно...
А то на сайте нету, предлагают писать и обсуждать. А мне что-то лень было в переписку вступать...
[00:55:27] <ada_ru> (Максим) Есть у них continues release, который вроде как подешевле
[00:55:55] <ada_ru> (vasil_sd) отвечает (Максим) на <Есть у них continues…>
А можно ссылку? Я на сайте про такое не видел
[00:56:16] <ada_ru> (vasil_sd) отвечает (Максим) на <Есть у них continues…>
За счет того, что являешься бесплатным бета-тестером? :)))
[00:59:53] <ada_ru> (Максим) GNAT Pro Comparison - AdaCore
https://www.adacore.com/gnatpro/comparison
[01:00:26] <ada_ru> (Максим) Gnat pro developer
[01:01:33] <ada_ru> (vasil_sd) отвечает (Максим) на <Gnat pro developer>
Ясно.
Под continues release имелось ввиду "Continuous patched releases" ?
[01:02:34] <ada_ru> (Максим) отвечает (vasil_sd) на <За счет того, что яв…>
Нет, просто поддержка по проще, время ответа не 2 дня, а 5. Тебе не предлагают wavefront-ы и твои багирепорты не секретные
[01:03:01] <ada_ru> (vasil_sd) Что такое wavefront?
[01:04:18] <ada_ru> (Максим) Это сборка продуктов из последних исходников после исправления ошибки (если тесты отработали нормально)
[01:04:43] <ada_ru> (Максим) отвечает (vasil_sd) на <Ясно.
Под continues…>
Да, его выпускают время от времени
[01:04:51] <ada_ru> (vasil_sd) отвечает (Максим) на <Это сборка продуктов…>
То есть багфиксы чуть медленнее докатываются?
[01:05:37] <ada_ru> (Максим) Да, и по-моему доступен только самый последний релиз, без истории
[01:06:13] <ada_ru> (vasil_sd) Для девелоперов нет gnatstack. Жаль, интересно было бы посмотреть на него...
[01:09:06] <ada_ru> (Максим) Никогда не использовал, впрочем я и spark не юзаю тоже 🙁
[01:09:46] <ada_ru> (vasil_sd) А CodePeer и SparkPro совсем отдельно идут? То есть, чтобы посмотреть всю доступную экосистему в полнофункциональном варианте, нужно аж несколько продуктов покупать?
[01:10:43] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <А CodePeer и SparkPr…>
наверно чтобы посмотреть, то проще всего зайти со стороны универов
[01:10:46] <ada_ru> (I_vlxy_I) IMHO
[01:10:49] <ada_ru> (Максим) 🤷♀ я не знаю
[01:11:12] <ada_ru> (Максим) Да, универам дают кажется всё
[01:12:01] <ada_ru> (vasil_sd) отвечает (Максим) на <Да, универам дают ка…>
Осталось только найти универ и попробовать договориться :))
Аспирантом, что-ли опять пойти.... :)))
[01:12:16] <ada_ru> (I_vlxy_I) или преподом 🙂
[01:13:23] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <или преподом 🙂>
Неее. Уже есть опыт... Не моё это - что-то рассказывать спящей аудитории... :)
А ещё лабы и экзамены с зачётами - это тихий ужос. Чур меня :)
[01:20:01] <ada_ru> (Максим) В принципе жпс и из исходников собрать можно. Я делал даже скрипт для Travis ci, но он не успевал отрабатывать за доступные бесплатно 50 мин и я его удалил
[01:22:22] <ada_ru> (vasil_sd) отвечает (Максим) на <В принципе жпс и из …>
Да, есть такая мысль. Может даже отважусь на это :)
А то руки чешутся некоторые баги поправить, которые мелкие, но сильно раздражают (падение при поытке настроить флаги PrettyPrint'ера и тд.)
[01:24:14] <ada_ru> (vasil_sd) А и в gnatstub есть бага, когда он не может сделать тела функций из спеки, если в спеке есть use директива...
[01:27:32] <ada_ru> (Максим) Gnatstub заменили на lalstab, вообще asis удалили, почти везде.
[01:28:33] <ada_ru> (Максим) Ну имя екзешника оставили, конечно, но переписали с нуля.
[01:29:28] <ada_ru> (vasil_sd) отвечает (Максим) на <Gnatstub заменили на…>
Да, оно где-то во внутренностях lal и падает. Там не ту операцию пытается применить к дереву ast
[01:29:31] <ada_ru> (Максим) Он теперь умеет добавлять тело для новой подпрограммы в имеющийся пакет
[01:30:00] <ada_ru> (vasil_sd) отвечает (Максим) на <Он теперь умеет доба…>
Не всегда :)))
Только при удачном стечении обстоятельств :)))
[01:30:40] <ada_ru> (Максим) Можно слать баг репорты пулиреквесты ☺️
[01:30:59] <ada_ru> (vasil_sd) отвечает (Максим) на <Он теперь умеет доба…>
Ещё пару раз косяки с параметрами добавленного тела были.
В общем, у меня он чаще не работает совсем
[01:32:03] <ada_ru> (vasil_sd) отвечает (Максим) на <Можно слать баг репо…>
Ну как соберу его локально, буду снимать хорошие дампы и либо патчи делать, если не сложно, либо хорошие репорты с тест-кейсами
[01:32:10] <ada_ru> (Максим) Да, лал молодая технология, если в самом gnat всё ещё ошибки вылазят, что уж тут
[01:32:48] <ada_ru> (vasil_sd) отвечает (Максим) на <Да, лал молодая техн…>
Фронтенд тоже на lal переделывается?
[01:33:10] <ada_ru> (Максим) НЕТ
[01:34:06] <ada_ru> (vasil_sd) отвечает (Максим) на <НЕТ>
Значит я пока недопонимаю немного.
А как lal с фронтендом компилятора тогда соотносится? Они независимы?
[01:34:38] <ada_ru> (Максим) Никак, это полностью с нуля написанная хрень
[01:36:40] <ada_ru> (vasil_sd) отвечает (Максим) на <Никак, это полностью…>
Понятно. То есть регулярно будут грабли от несоответствия lal фронтенду.
[01:37:04] <ada_ru> (Максим) ASIS работал с деревом фронтенда, но стал начальству поперёк горла и его заменили на это чудо природы
[01:37:21] <ada_ru> (vasil_sd) отвечает (Максим) на <ASIS работал с дерев…>
А кстати почему?
[01:37:32] <ada_ru> (Максим) 🤷♂
[01:38:07] <ada_ru> (vasil_sd) Технических причин нет, политика?
[01:38:53] <ada_ru> (Максим) Сам не пойму. Asis я знаю и может по этому люблю, а лал хрень какая-то
[01:40:48] <ada_ru> (vasil_sd) Странное, на мой взгляд, решение получается - много возни будет с постоянной синхронизацией того как конструкции языка видит компилятор и как lal.
[01:40:59] <ada_ru> (I_vlxy_I) На ASIS ещё и стандарт же был
[01:41:19] <ada_ru> (I_vlxy_I) А теперь чисто адокоровское поделие будет :-)
[01:41:27] <ada_ru> (I_vlxy_I) Освобождение от оков!
[01:41:35] <ada_ru> (Максим) отвечает (I_vlxy_I) на <На ASIS ещё и станда…>
Да, Лалу до стандарта далеко
[01:41:42] <ada_ru> (I_vlxy_I) Ну и питончика побольше!
[01:41:51] <ada_ru> (vasil_sd) отвечает (Максим) на <Сам не пойму. Asis я…>
А ASIS совсем везде выпиливать будут и забросят?
[01:42:21] <ada_ru> (Максим) Уже выпиляли, в январе
[01:42:23] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Ну и питончика побол…>
Жесть... В экосистему ады пускать всяких гадов... :)
[01:42:55] <ada_ru> (I_vlxy_I) <прислал наклейку> 🐍
[01:43:58] <ada_ru> (vasil_sd) отвечает (Максим) на <Уже выпиляли, в янва…>
Блин. Видать и до AdaCore эффективные менеджеры добрались... :(
Теперь всё будет модно и молодёжно, питон, JS, что там ещё популярно?
[01:45:00] <ada_ru> (Максим) Зато к Лалу есть биндинг на ocaml! 😂
[01:46:21] <ada_ru> (vasil_sd) отвечает (Максим) на <Зато к Лалу есть бин…>
Эка невидаль. Можно было и к ASIS биндинги сделать. OCaml относительно легко биндится с нативно-компилируемыми языками.
[01:46:22] <ada_ru> (Максим) Скоро codepeer будет ещё лучше из-за этого!
[01:46:35] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Блин. Видать и до Ad…>
rustRustRUST! Как замена непопулярной Ады
[01:46:53] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <rustRustRUST! Как за…>
Нечего, и до раста доберутся :)))
[01:47:13] <ada_ru> (Максим) отвечает (I_vlxy_I) на <rustRustRUST! Как за…>
Теперь я пойду спать
[01:47:17] <ada_ru> (I_vlxy_I) Растакор!
[01:47:53] <ada_ru> (Лекс) отвечает (I_vlxy_I) на <Растакор!>
👍🏻
[01:48:08] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Растакор!>
Для снижения порога входа и дешёвых программистов сделают что-то типа PytoRust'a (Python + Rust) :)
[01:49:05] <ada_ru> (I_vlxy_I) Раст вообще неплохо подходит для спаривания его с другими технологиями :-)
[01:49:33] <ada_ru> (I_vlxy_I) По крайней мере в плане названий
[01:49:45] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <По крайней мере в пл…>
:)
[01:49:49] <ada_ru> (I_vlxy_I) Плюсораст! (Firefox)
[01:50:11] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Плюсораст! (Firefox)>
:))))
[01:50:36] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Плюсораст! (Firefox)>
Яндексоид мечтающий писать на расте :)
[01:50:56] <ada_ru> (I_vlxy_I) :-)
[01:53:18] <ada_ru> (Лекс) отвечает (I_vlxy_I) на <:-)>
можно я на этом канале пропиарю свой канал? (полный оффтоп, тематика — бизнес )
[01:53:33] <ada_ru> (I_vlxy_I) Ну, с учетом того, что у адакоры есть инструментарий и продукты даже для разработки на с++, очевидно, что и для раста что-то будет, если это будет выгодно и будет спрос со стороны Клиентов.
[01:53:56] <ada_ru> (I_vlxy_I) Rust на vxworks - первый звоночек
[01:54:00] <ada_ru> (I_vlxy_I) IMHO
[01:54:26] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Ну, с учетом того, ч…>
Вот зря они плюсы тянут. Лучше бы сразу раст затягивали в экосистему...
[01:55:31] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Вот зря они плюсы тя…>
Долгое время альтернативы плюсам совсем не было. Ну и Раст он таки на llvm, а плюсы у них через gcc таки. Общая база с gnat и одни исходники
[01:56:52] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Долгое время альтерн…>
Ну gnat потихоньку уже и на llvm обживается.
А с llvm в своё время Столлман знатно промахнулся... Могла бы история совсем по другому пути пойти...
[01:58:19] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Долгое время альтерн…>
В области специализации AdaCore плюсы - это не тот язык который стоит поддерживать.
[01:58:51] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <В области специализа…>
Если Боинг хочет, то адакор делает
[01:59:13] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Если Боинг хочет, то…>
Боинг вон уже как нахотел... Как бы совсем не загнулся
[01:59:15] <ada_ru> (I_vlxy_I) F-35 это уже плюсы. И это хороший заказчик
[01:59:43] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <F-35 это уже плюсы. …>
Эх... Везде политика, распилы и откаты...
[02:00:20] <ada_ru> (I_vlxy_I) И последующие тоже будут или плюсы или что-то ещё. То, что вернётся на Аду - маловероятно. IMHO
[02:01:33] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <И последующие тоже б…>
Большая ошибка недальновидных менеджеров. В желании сэкономить на программистах, они потратят гораздо больше (ну либо у них нет цели нормально проект сделать).
[02:02:03] <ada_ru> (vasil_sd) Насколько я помню у F-35 дохрена проблем и он просто фантастически дорогой
[02:02:15] <ada_ru> (I_vlxy_I) Там кода сильно больше
[02:02:28] <ada_ru> (I_vlxy_I) Ну и там не только в коде проблемы
[02:02:59] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Там кода сильно боль…>
Вот поэтому и нельзя было плюсы брать. По моим наблюдениям плюсы для крупных проектов очень плохо подходят
[02:03:05] <ada_ru> (I_vlxy_I) На Аде код писали бы до сих пор - нет столько Ада программистов, чтобы написать столько
[02:03:51] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <На Аде код писали бы…>
Плюсовики на Аду переучиваются быстро. Чуть больше чем по рынку предложить - и думаю проблем не будет.
[02:04:25] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Плюсовики на Аду пер…>
Даёшь доклад про Аду на с++ дринкапе!
[02:04:53] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Даёшь доклад про Аду…>
Интересная идея :)
[02:06:11] <ada_ru> (vasil_sd) Где-то были видео про тётеньку, заядлую плюсовичку, которая даже книжек каких-то понаписала.
Так вот, она недавно для себя открыла Аду и теперь везде её пропагандирует вместо плюсов (ибо хорошо представляет себе, что такое плюсы)
[02:06:25] <ada_ru> (vasil_sd) Сейчас поищу, может найду...
[02:07:52] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Интересная идея :)>
Адская!
[02:12:15] <ada_ru> (I_vlxy_I) Ладно, я спать.
[02:12:42] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Ладно, я спать.>
Я пожалуй тоже...
[02:14:00] <ada_ru> (vasil_sd) Во, нашёл таки: https://youtu.be/hgS_xPu8DyY
Всё, теперь точно спать :))
[04:25:44] <ada_ru> (a) В дайджест?
[05:13:32] <ada_ru> (a) http://www.opennet.ru/opennews/art.shtml?num=52177 про wasm
[13:24:25] <ada_ru> (I_vlxy_I) https://medium.com/@ssg/how-is-computer-programming-different-today-than-20-years-ago-9d0154d1b6ce
[13:24:43] <ada_ru> (I_vlxy_I) «A package management ecosystem is essential for programming languages now. People simply don’t want to go through the hassle of finding, downloading and installing libraries anymore. 20 years ago we used to visit web sites, downloaded zip files, copied them to correct locations, added them to the paths in the build configuration and prayed that they worked.»
[13:25:19] <ada_ru> (I_vlxy_I) К вопросу о том, что gprbuild достаточно
[13:25:38] <ada_ru> (I_vlxy_I) Было достаточно - 20 лет назад
[14:37:33] <ada_ru> (Oleg) conf t
[14:57:53] <ada_ru> (Максим) отвечает (I_vlxy_I) на <А на сайте alire где…>
https://alire.ada.dev/crates/matreshka_league.html
[15:00:04] <ada_ru> (I_vlxy_I) отвечает (Максим) на <https://alire.ada.de…>
Круто!
[15:00:17] <ada_ru> (I_vlxy_I) А что значит * у make?
[15:01:48] <ada_ru> (I_vlxy_I) Оу! А через alire можно прям gnat поставить? https://alire.ada.dev/crates/gnat.html
[15:01:59] <ada_ru> (Максим) ну это перечень зависимостей для сборки
[15:02:24] <ada_ru> (I_vlxy_I) отвечает (Максим) на <ну это перечень зави…>
Это я понимаю, но почему там звездочка?
[15:03:03] <ada_ru> (Максим) отвечает (I_vlxy_I) на <Оу! А через alire мо…>
Нет, там всё в кучу, "нативные" пакеты, которые ты сам должен поставить (типа make) и Ада пакеты которые собираются из исходников
[15:04:32] <ada_ru> (I_vlxy_I) А если я скажу alr get —build gnat или make?
[15:05:37] <ada_ru> (Максим) отвечает (I_vlxy_I) на <Это я понимаю, но по…>
я не знаю 😕
[15:06:40] <ada_ru> (Максим) max@untu:/tmp/alire$ ~/bin/alr get --build gnat
ERROR: The requested version (gnat=0.0.0) is not available
ERROR: You can retrieve it without dependencies with --only
ERROR: alr get unsuccessful
[15:13:03] <ada_ru> (I_vlxy_I) :-(
[15:13:14] <ada_ru> (I_vlxy_I) Неконсистентно ...
[15:15:53] <ada_ru> (Максим) Перепили на conan, ты же шаришь в нём 😊
[15:28:38] <ada_ru> (I_vlxy_I) Посмотрел на биндинги к sdl у раста - там тоже печально. Надо руками ставить sdl. Правда там добавили опцию, когда при сборке биндинга оно само лезет в интернет и выкачивает сорцы sdl и собирает их
[15:32:30] <ada_ru> (I_vlxy_I) Плохой Раст! Пойду посмотрю как это сделано в адекватных языках
[15:33:46] <ada_ru> (Oleg) отвечает (I_vlxy_I) на <Плохой Раст! Пойду п…>
😊 это в каких ?
[16:15:55] <ada_ru> (Лекс) Немного оффтопа, хотя здесь почти всё оффтоп, но ладно 😃
Все ведь знают про такой язык? https://www.red-lang.org
[17:02:10] <ada_ru> (Eugene) отвечает (Лекс) на <Немного оффтопа, хот…>
ну я читал этот сайт, но не впечатлился, для своих задачек применения не нашёл...
а что?
[17:07:07] <ada_ru> (Лекс) А я впечатлился, ещё несколько лет назад.
Как по мне, так крутая тема — кросплатформенная фуллстек среда разработки, ещё и в мегабайтном бинаре.
Один только DSL UI шедевр, неговоря уже про тему Red => Red/System.
Да и rebol кстати впечатлил, код небольшой и выразительный, имхо — самое оно для бизнеса, жаль что загнулся
Правда применить до сих пор было негде
[17:14:15] <ada_ru> (I_vlxy_I) отвечает (Oleg) на <😊 это в каких ?>
Есть подозрение, что js o_O
[17:14:44] <ada_ru> (I_vlxy_I) отвечает (Лекс) на <А я впечатлился, ещё…>
Динамическая типизация должна умереть
[17:14:49] <ada_ru> (I_vlxy_I) В корчах!
[17:15:55] <ada_ru> (vasil_sd) отвечает (Лекс) на <А я впечатлился, ещё…>
Некоторые варианты Форта были интереснее... :)
[17:16:03] <ada_ru> (I_vlxy_I) 💻 РЖД закупят для своих подразделений 15 000 отечественных компьютеров
На это потратят 1 млрд рублей. Это станет крупнейшей в России закупкой ПК на отечественных процессорах
[17:16:39] <ada_ru> (Oleg) А в расте как с формальной верификацией
[17:16:41] <ada_ru> (Oleg) ?
[17:19:03] <ada_ru> (Лекс) отвечает (Oleg) на <А в расте как с форм…>
судя по гуглингу — никак, даже в сях лучше ибо есть обкатанная Frama-C
[17:20:15] <ada_ru> (I_vlxy_I) отвечает (Oleg) на <А в расте как с форм…>
А оно нужно? То есть для большинства применений оно не нужно.
[17:20:40] <ada_ru> (I_vlxy_I) Мал шанс, что с этим придётся столкнуться в реальной жизни
[17:20:55] <ada_ru> (Oleg) Если хочется то можно
[17:21:17] <ada_ru> (vasil_sd) отвечает (Лекс) на <судя по гуглингу — н…>
Мой опыт работы с фрамой-си говорит о том, что она даалеко не обкатанная. Там чуть в сторону от тривиальных вещей и уже начинаются проблемы.
[17:22:26] <ada_ru> (Лекс) Под обкаианная я имел в виду "прожила хоть сколько-то", к тому же видел её в каких-то проектах (чуть больше доморощеных)
[17:25:06] <ada_ru> (I_vlxy_I) А у Ады с этим как?
[17:25:11] <ada_ru> (vasil_sd) отвечает (Лекс) на <Под обкаианная я име…>
Ну если в таком смысе, то да.
Я как-то пытался доказать свойства одного сишного кода, которые без проблем доказал в эквиваленте SPARK/GnatProve, и не смог.
Там были ошибки трансляции WP в why3. Тупо потеряли при трансляции переменные-призраки и часть логики.
[17:25:44] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <А у Ады с этим как?>
У Ады с этим хорошо.
SPARK/GnatProve позволяют иногда доказывать весьма нетривиальные вещи
[17:26:23] <ada_ru> (vasil_sd) На одной из прошлых работ я доказал серьёзные свойства кода по межпроцессорному обмену сообщений.
[17:27:08] <ada_ru> (vasil_sd) отвечает (vasil_sd) на <На одной из прошлых …>
Кстати именно его пробовал доказать в сишном варианте с фрамой-си и не смог. Тогда фрама показалась ещё очень сырой и не для промышленного применения.
[17:28:11] <ada_ru> (Лекс) отвечает (vasil_sd) на <Кстати именно его пр…>
А ещё что-нибудь для C/C++ есть?
[17:29:06] <ada_ru> (vasil_sd) отвечает (Лекс) на <А ещё что-нибудь для…>
Много чего есть, если не циклиться на логике Хоара и производных, то есть модел-чекинг неплохой. Есть KLEE и тд
[19:06:26] <ada_ru> (Максим) Ради klee, кажется, Адакор и пилит gnat-llvm. (Но это не точно 😋)
[19:12:15] <ada_ru> (vasil_sd) отвечает (Максим) на <Ради klee, кажется, …>
KLEE очень интересная штука. Только я ещё с ней не пробовал что-нибудь серьёзное делать.
А LLVM давно уже жду, если GNAT будет полноценно поддерживать LLVM - это такие перспективы открываются...
[22:15:36] <ada_ru> (Oleg) Это точно , и я жду
[22:15:54] <ada_ru> (I_vlxy_I) С лицензиями там не очень
[22:15:57] <ada_ru> (a) отвечает (I_vlxy_I) на <💻 РЖД закупят для св…>
1 000 000 000/15 000= 66 666. 66667 символично
[22:16:17] <ada_ru> (I_vlxy_I) Вахаха!
[22:16:48] <ada_ru> (a) Трижды число зверя, не?
[22:17:53] <ada_ru> (I_vlxy_I) И семерка в конце!
[23:05:43] <ada_ru> (I_vlxy_I) но вообще, 66тыр за отечественный это очень норм. если это реально отечественный эльбрус какой, а не переклеенный шилдик
[23:20:03] <ada_ru> (Oleg) Да и правильно, хоть деньги в стране останутся
[23:20:10] <ada_ru> (Oleg) Хотя не уверен :-)
[23:45:41] <ada_ru> (Лекс) Пихоно-проблемы