[00:51:59] <ada_ru> (Максим) VerifyThis Challenge in SPARK - The AdaCore Blog
https://blog.adacore.com/verifythis-challenge-in-spark
[00:52:06] <ada_ru> (Максим) Это не оно?
[11:52:29] <ada_ru> (Eugene)  отвечает (Максим) на <Это не оно?>
да, судя по описанию -- то самое, осталось понять описание и программу )))
[11:57:42] <ada_ru> (I_vlxy_I)  отвечает (Eugene) на <да, судя по описанию…>
Будто в Идрисе не надо понять :-)
[11:59:37] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <Будто в Идрисе не на…>
ну что, ты уже начал писать код на с++? )))
[12:00:15] <ada_ru> (Eugene) наверняка на с++ тоже можно сделать подобное, ведь там даже тетрис в режиме компиляции смогли запустить
[12:01:29] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <Будто в Идрисе не на…>
ада/спарк выгодно отличаются от идриса тем, что они -- промышленное решение, а идрис, увы, не готов к продакшину
[12:13:06] <ada_ru> (I_vlxy_I) И без зависимых типов!
[12:14:05] <ada_ru> (I_vlxy_I)  отвечает (Eugene) на <ну что, ты уже начал…>
А ты мне простой пример то опиши :-) А не вундервафлю из сотен строк кода :-)
[12:57:03] <ada_ru> (I_vlxy_I) А вот миллионы вебсоцкётов на гоу
[12:57:09] <ada_ru> (I_vlxy_I) Hi, channel 👋
You probably know, how to deal with WebSockets in Go, don’t you?
But what if we need to handle millions of them? In the following well-written article an approach is described which could help us to handle up to 3 million online connections 😱

https://www.freecodecamp.org/news/million-websockets-and-go-cc58418460bb/
[13:02:01] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <А ты мне простой при…>
так вся формальная верификация такая -- простой пример превращается в вундервафли на сотни строк кода )))
[13:06:18] <ada_ru> (I_vlxy_I)  отвечает (Eugene) на <так вся формальная в…>
Простой пример с зависимыми типами. Не обязательно желающий что-то полезное.
[13:55:18] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <Простой пример с зав…>
ну вот простой пример (идрис)
допустим, есть список, у которого в типе зашит не только тип элементов, но и количество элементов: Vect n elem
нужно написать функцию конкатенации двух таких списков, в типе которой будет указано, что длина результирующего списка равна сумме длин входных списков:

append : Vect n elem -> Vect m elem -> Vect (n + m) elem

нужно написать заготовку реализации этой функции:

append [] ys = ?append_rhs_1
append (x :: xs) ys = ?append_rhs_2

компилятор достаточно умён, что бы вывести из типа этой функции реализацию этой заготовки:

append : Vect n elem -> Vect m elem -> Vect (n + m) elem
append [] ys = ys
append (x :: xs) ys = x :: append xs ys  

это простейший пример, более сложный пример должен бы включать указание, что выходной список содержит все элементы входных списков в порядке, в котором они там были, ну и всякое такое...
[14:18:00] <ada_ru> (Лекс) звучит не плохо, и вроде даже понятно 😃
[14:20:17] <ada_ru> (Лекс) Меня только немного смущает, то, что нужно доказывать что в выходном списке элементы находятся в том же порядке в котором и вошли О_0 т.е. тот факт что может быть иначе, это вообще как и зачем >_<

Формальная верификация по моему нужна для вещей по важнее: доказывать соответствие программной реализации математической модели алгоритма, что сейчас вообще говоря встречается не так часто, как всякие игрулички с верификацией не пойми чего типа аля чтобы деления на ноль небыло
[14:24:12] <ada_ru> (Eugene)  отвечает (Лекс) на <Меня только немного …>
ну, такие требования зависят от постановки задачи -- где-то нужно, где-то не нужно...
[14:25:11] <ada_ru> (Eugene) вот зависимые типы как раз и прелагают, что бы формальная модель записывалась в виде типов, а затем с помощью этих типов можно было бы вывести реализацию и/или доказать корректность реализации
[14:27:12] <ada_ru> (Лекс) обычно все примеры на хаскеллах и подобном это как раз приводят на чём-то бесполезном и складывается соответствующее впечатление
[14:28:10] <ada_ru> (Eugene) так на полезном там столько кода будет, что никто смотреть не станет ))
[14:28:41] <ada_ru> (Eugene) это как с ООП -- вся мощь и полезность ООП проявляется на больших программных проектах, а на микропримерчиках фигня выходит
[14:34:12] <ada_ru> (I_vlxy_I)  отвечает (Eugene) на <это как с ООП -- вся…>
На больших у ООП тоже часто фигня выходит. Поубивал бы.
[17:19:12] <ada_ru> (I_vlxy_I) Хм. Опять в Бельгии адские вакансии
[17:19:20] <ada_ru> (I_vlxy_I) Аж две штуки
[17:23:13] <ada_ru> (Максим) В самолётах! 😊
[17:29:47] <ada_ru> (I_vlxy_I) Не прогрессивные какие-то. Надо им пояснить за питон, js и современные подходы к разработке.
[19:17:36] <ada_ru> (Oleg) Не надо, вдруг там появится что-то интересное
[19:17:45] <ada_ru> (Oleg) А не эти ваши жс
[19:18:16] <ada_ru> (Oleg) Скинь ссылки
[19:18:33] <ada_ru> (Oleg) Изучу срочно аду и махну в Бельгию :-)
[19:18:44] <ada_ru> (iserged)  отвечает (I_vlxy_I) на <Аж две штуки>
Этом потому что там тонна легаси, который уже никто не понимает, чтобы переписать. А потом они падают
[19:19:29] <ada_ru> (Oleg) В 1988 году мы с семьей жили месяц или два в бельгийском посольстве
[19:19:39] <ada_ru> (Oleg) Или в 89 не помню уже
[19:20:09] <ada_ru> (Oleg) Помню Ван Гейер там был и я ещё ребёнок с ним играл в шахматы
[19:21:08] <ada_ru> (I_vlxy_I)  отвечает (Oleg) на <Скинь ссылки>
https://www.reddit.com/r/ada/comments/eej1n9/ada_job_belgium_brussels_aviation_sector/
[19:22:36] <ada_ru> (Oleg) Спасибо
[19:23:24] <ada_ru> (Oleg) Ещё помню в выходные к нему приезжали друзья голландцы и пили пиво :-)
[19:23:56] <ada_ru> (Oleg) Прямо на рабочем месте :-) ну он там и жил правда
[19:24:12] <ada_ru> (I_vlxy_I) :-)
[19:26:59] <ada_ru> (Oleg) Кстати наблюдаю нехорошую тенденцию
[19:27:21] <ada_ru> (Oleg) IOS XR took its first steps in this direction by moving from a 32-bit QNX operating system to a 64-bit Linux operating system with a strong focus on operational features that could help meet the requirements of the industry.
[19:27:54] <ada_ru> (Oleg) Все скатывается к одной системе и это linux в котором масса не очень хороших решений
[19:28:06] <ada_ru> (Oleg) И масса конечно очень хороших
[19:28:40] <ada_ru> (Oleg) Но это не отменяет того факта что в некоторых приложениях BSD/QNX выгоднее смотрится
[19:29:27] <ada_ru> (I_vlxy_I) Да, так уже было в разных областях. И это всегда плохо заканчивалось
[19:54:54] <ada_ru> (Лекс) Бизнес, его задача зарабатывать больше минимизируя расходы. А современный бизнес очень социопатичен, наплевать всем и на прогресс, и на надежность, и даже на удобность.

Тимлиды выбирают решения где проще и дешевле найти замену, то что массовее
[19:59:09] <ada_ru> (I_vlxy_I)  отвечает (Лекс) на <Бизнес, его задача з…>
js! Все там будем
[20:01:37] <ada_ru> (Oleg) Да это то понятно, такова жизнь, у меня тоже бизнес но модель пока другая
[20:12:04] <ada_ru> (Лекс)  отвечает (I_vlxy_I) на <js! Все там будем>
Разве ещё не все?😂
[20:12:30] <ada_ru> (Лекс) Спросил я из телеграма на электрончике
[20:12:54] <ada_ru> (I_vlxy_I)  отвечает (Лекс) на <Спросил я из телегра…>
Он не на электроне если что
[20:13:27] <ada_ru> (I_vlxy_I) Он на Qt/c++ под виндами и линуксом и на свифте и нативный под макосью
[20:13:35] <ada_ru> (Лекс) А на чём? По ощущениям очень даже на хроме каком-то
[20:14:55] <ada_ru> (I_vlxy_I) Я написал :-)
[20:18:52] <ada_ru> (Oleg) Ну вот слек хз на чем но тормоз
[20:19:24] <ada_ru> (Oleg) Питерский Мегафон если что пообещал опять инет шатать с часа ночи
[20:19:45] <ada_ru> (Oleg) Если у кого их каналы имейте ввиду
[20:24:36] <ada_ru> (Лекс)  отвечает (Oleg) на <Ну вот слек хз на че…>
На js родном 😂
[20:46:03] <ada_ru> (I_vlxy_I)  отвечает (Лекс) на <На js родном 😂>
Все там будем...
[21:31:11] <ada_ru> (Oleg) Что там за беспредел про Яндекс такси рассказывают :-)
[21:32:27] <ada_ru> (I_vlxy_I)  отвечает (Oleg) на <Что там за беспредел…>
Ы?
[21:33:18] <ada_ru> (Oleg) Да типа деньги списывают за просто так
[21:33:39] <ada_ru> (Oleg) Двухфакторной аутентификации то нет...
[21:34:04] <ada_ru> (Oleg) Это все C++ виноват :-)))) надо было на АДА все делать !
[21:43:26] <ada_ru> (Лекс) на TypeScript же
[21:43:47] <ada_ru> (Лекс) или сразу на жс, чтобы наверняка, ато малоли скомпелируется ещё не надёжно
[21:58:31] <ada_ru> (Oleg) https://www.google.ru/amp/s/m.habr.com/ru/amp/post/480604/
[21:58:40] <ada_ru> (Oleg) Шикарно :-)
[21:59:16] <ada_ru> (Oleg) В 2000 такое уже было с мониторами
[22:00:59] <ada_ru> (Oleg) И я как бы не против , но сделайте хоть прилично, договоритесь с OEM поставщиками и так далее
[22:05:42] <ada_ru> (Лекс) это же: 1. расходы 2. бумака-марака
[22:09:33] <ada_ru> (I_vlxy_I)  отвечает (Oleg) на <В 2000 такое уже был…>
Но не у нас, а в Белоруссии
[22:10:18] <ada_ru> (Лекс) Интеграл или как его там 😃
[22:15:19] <ada_ru> (Oleg) Не, именно у нас
[22:15:34] <ada_ru> (Oleg) Альфа компьютерс их продавала
[22:15:47] <ada_ru> (Oleg) Непомню уже как назывались
[22:16:30] <nordwind> Маяк,  каяк, ху*к, ху*к и в продакшн... Норма же
[22:16:53] <ada_ru> (Oleg) А я смотрю все ОС на аде загнулись ?
[22:17:06] <ada_ru> (Oleg) Пейчаль
[22:18:58] <nordwind> /me снова починил радио и слушает маяк :)
[22:21:45] <nordwind> Нафиг аду
[22:22:36] <nordwind> Вон новый Раст вышел, что то вы не обсуждаете, странно даже
[22:22:55] <nordwind> На опеннете анонс
[22:29:21] <ada_ru> (a)  отвечает (Oleg) на <Питерский Мегафон ес…>
https://m.habr.com/ru/news/t/481682/ ? Не оно?
[22:30:27] <ada_ru> (Oleg) Да может и оно, может врут по телефону , это ж Мегафон
[22:33:19] <ada_ru> (I_vlxy_I)  отвечает на <(nordwind) Вон новый…>
Дык я уже форвардил новость :-)
[22:34:28] <ada_ru> (I_vlxy_I) С хабра вроде
[22:50:23] <ada_ru> (Eugene)  отвечает (Oleg) на <А я смотрю все ОС на…>
да скоро тока плюникс один останется
[23:16:25] <ada_ru> (I_vlxy_I) да, винда падёт!
[23:20:17] <ada_ru> (Oleg) Бесспорно а жаль
[23:20:29] <ada_ru> (Eugene) винда 10 мобайл уже всё
[23:26:33] <ada_ru> (I_vlxy_I) да и десктопная винда чем дальше, тем больше линукс с гугл хромом
[23:26:38] <ada_ru> (I_vlxy_I) и рекламой
[23:55:41] <ada_ru> (a) Куда падёт винда? На головы еретиков и отступников?