[00:00:09] <ada_ru> (vasil_sd) отвечает (Oleg) на <Ну тогда думаю раст …>
Хотя да, если строчек 500-700 то тут и раст может выиграть. Ибо размер мелкий и можно написать криво и косо, даже не вникая в borrowing и пр.
[00:02:22] <ada_ru> (Oleg) Для человека кто не изучал Паскаль или как я VHDL думаю все будет совсем чуждо. А в расте более менее все стильно/модно/молодёжно
[00:03:01] <ada_ru> (I_vlxy_I) да ладно, паскаль от си вообще не отличается
[00:03:07] <ada_ru> (Oleg) В принципе нормальному программисту будет все равно спустя какой нибудь месяц/два
[00:03:19] <ada_ru> (vasil_sd) отвечает (Oleg) на <Для человека кто не …>
Непривычно - да. Но семантически ближе Ада к плюсам, чем раст.
[00:03:41] <ada_ru> (Oleg) отвечает (vasil_sd) на <Непривычно - да. Но …>
Да, но с первого взгляда и не скажешь :-)
[00:04:19] <ada_ru> (Oleg) Раст мне лично немного сложно осваивать пока
[00:04:39] <ada_ru> (Oleg) Но коммунити там конечно живее нас
[00:04:44] <ada_ru> (vasil_sd) отвечает (Oleg) на <Да, но с первого взг…>
Синтаксис с толку просто сбивает.
[00:05:11] <ada_ru> (Oleg) 100500 человек в чате у них :-)
[00:05:24] <ada_ru> (I_vlxy_I) 1700 всего - в два раза меньше плюсов!
[00:05:27] <ada_ru> (vasil_sd) отвечает (Oleg) на <Раст мне лично немно…>
Раст легко понимать через призму теории типов. Borrowing - почти один в один линейные типы.
[00:07:07] <ada_ru> (vasil_sd) Кстати, насчёт раста - там же ещё вроде бы нельзя так хорошо рулить представлениями структур и типов как в аде?
[00:08:42] <ada_ru> (I_vlxy_I) А на каких задачах Ада лучше проявила бы себя чем Раст? встроенку не берем. проекты на 10 миллиардов строк кода тоже.
то есть какой поставить эксперимент, чтобы Ада там превзошла Раст?
[00:08:49] <ada_ru> (I_vlxy_I) на какой задаче?
[00:11:32] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <А на каких задачах А…>
Ада рулит на больших проектах с большим временем жизни. Точную границу тут найти тяжело.
Ещё Ада рулит там, где нужно точно определять представления структур данных (например системные регистры с битовыми полями, пакеты данных всякие и пр).
Ещё SPARK + GnatProve одни из наиболее развитых в индустрии. Можно что-нить из этой области придумать.
[00:11:59] <ada_ru> (sergey_dukov) философский вопрос на чём быстрее реализовать проект, много раз расматривался в литературе, начиная со статей и лекций Дейкстры. Показано, что этот вопрос не совсем правомочный. Если, скажем, коллектив программистов имеет большой опыт в реализации проектов на C++, то им не стоит переходить на АДУ или что то другое. Вопрос имеет много субъективных фактороров.
[00:12:22] <ada_ru> (I_vlxy_I) "Ада рулит на больших проектах с большим временем жизни. Точную границу тут найти тяжело."
это нефальсифицируемая гипотеза 🙁
[00:12:49] <ada_ru> (I_vlxy_I) "Ещё Ада рулит там, где нужно точно определять представления структур данных (например системные регистры с битовыми полями, пакеты данных всякие и пр)."
вот прямо про регистрам процессора раскидать можно? а как?
[00:13:42] <ada_ru> (I_vlxy_I) "программистов имеет большой опыт в реализации проектов на C++, то им не стоит переходить на АДУ или что то другое."
А кому стоит переходить на Аду? Когда стоит начинать проект на Аде вообще?
[00:13:46] <ada_ru> (vasil_sd) отвечает (sergey_dukov) на <философский вопрос н…>
Есть примеры в промышленности, когда переход на Аду давал существенный выигрыш. Сейчас точно не вспомню, но несколько лет назад читал очень интересную статью на этот счёт. Там большой проект переводили, по-моему, с Си.
[00:14:18] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <"Ада рулит на больши…>
это вообще не гипотеза, а IMHO :) Как и все остальные мои высказывания :)
[00:14:43] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <это вообще не гипоте…>
ок. твоё IMHO тут не фальсифицируемо 🙂
[00:15:20] <ada_ru> (I_vlxy_I) а хочется то экспериментального подтверждения хоть чего-то
[00:15:55] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <"Ещё Ада рулит там, …>
Я имел ввиду всякие memory mapped управляющие регистры и пр. Ада позволяет даже семантику доступа задавать к ним (типа сначала прочитать 64 бита, поменять пару бит и записать обратно сразу 64 бита)ю
[00:16:26] <ada_ru> (I_vlxy_I) у раста вот для проектов начинающихся есть турбобуст - cargo. он позволяет на этом бусте очень быстро достичь состояния прототипа работающего.
[00:17:07] <ada_ru> (I_vlxy_I) а если язык ХХХ начинает давать какой-то профит только начиная с 10 миллионов строк кода в проекте, то, боюсь, почти ни один проект на этом языке до этого состояния не дорастет.
[00:17:32] <ada_ru> (I_vlxy_I) высокая детская смертность у проектов на таком языке будет
[00:17:37] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <"программистов имеет…>
Я вот на праздниках мелкий проект (RAW файлы от S5Pro декодирую в полный диапазон) начал на Аде. Уже дописываю. Довольно быстро получается. Примерно 5 тыс строк уже.
[00:18:44] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <у раста вот для прое…>
Да Cargo - это очень сильно.
Для Ады нужно такое же с прямой поддержкой в gprbuild.
Или как в OCaml - OPAM.
[00:19:05] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Да Cargo - это очень…>
Ну, alire пилят
[00:20:10] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Ну, alire пилят>
Да, интересно. Не сталкивался пока, сейчас пойду смотреть, что это
[00:20:20] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Да, интересно. Не ст…>
https://alire.ada.dev
[00:20:31] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <https://alire.ada.de…>
Ага, спасибо, уже нашёл
[00:21:15] <ada_ru> (I_vlxy_I) но у меня была крамольная мысль, что коль скоро Ада активно юзает плюсовые либы и сишные либы, почему бы и не conan? 🙂
[00:21:31] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <https://alire.ada.de…>
и на первой же странице у них упомянуты cargo и opam :))
[00:21:40] <ada_ru> (sergey_dukov) А насчёт языков программирования показано, что все современные универсальные языки практически равноцены. А скорость кодирования зависит от конкретного программиста. Бывает так, что один программист реализует проекты на ассемблере гораздо быстрее чем несколько других на языках высокого уровня.
[00:21:58] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <и на первой же стран…>
ну, с учетом того, что SPARK писан на OCaml... 🙂
[00:22:48] <ada_ru> (I_vlxy_I) отвечает (sergey_dukov) на <А насчёт языков прог…>
кроме того, современные исследования не смогли выявить и значимую разницу в надежности ПО на разных ЯП
[00:23:06] <ada_ru> (vasil_sd) отвечает (sergey_dukov) на <А насчёт языков прог…>
Слишком сильное утверждение. По каким параметрам равноценны? Тьюринг-полнота не в счет.
[00:25:00] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <кроме того, современ…>
Тут есть фактор анализируемости языков. Есть языки с формально определённой семантикой, которые можно автоматически анализировать (в смысле математические свойства программ на этих ЯП). А есть, для которых такой анализ практически (иногда даже теоретически) невозможен.
[00:25:48] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Тут есть фактор анал…>
не, я про экспериментальное подтверждение. анализ проектов на разных ЯП не выявил существенной разницы.
[00:26:04] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <ну, с учетом того, ч…>
Там на OCaml alt-ergo и why3, а сам gnatprove на аде. SPARK - это вообще язык
[00:26:27] <ada_ru> (I_vlxy_I) может быть то был хреновый анализ. но других не завезли
[00:26:34] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <не, я про эксперимен…>
Интересно. А есть ссылка на этот анализ?
[00:26:46] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Там на OCaml alt-erg…>
я знаю что SPARK это язык
[00:27:37] <ada_ru> (sergey_dukov) Ну тут расписываете преимуществе АДЫ в управлении типами, и приводятся конкретные примеры, но всё это (повторяю всё!) присутствует в C++!
[00:28:45] <ada_ru> (vasil_sd) отвечает (sergey_dukov) на <Ну тут расписываете …>
Не всё.
Задать побитово расположение полей структуры в памяти на плюсах весьма нетривиальная задача, которая решается языковыми средствами через метапрограммирование на шаблонах.
А в Аде это из коробки.
[00:29:42] <ada_ru> (vasil_sd) Вот такое https://www.adaic.org/resources/add_content/standards/05aarm/html/AA-13-5-1.html#S0289
На плюсах весьма нетривиально делается
[00:30:35] <ada_ru> (vasil_sd) Похожую задачу на плюсах я решал когда-то примерно так: https://github.com/vasil-sd/cpp-bits/blob/master/bitops.h
[00:31:07] <ada_ru> (vasil_sd) Разница весьма существенна в объёме писанины и в дальнейшей поддержке кода
[00:31:23] <ada_ru> (vasil_sd) Ну и много других примеров могу привести
[00:32:12] <ada_ru> (sergey_dukov) Да нет. Задание битовых полей и их длин есть в реликтовом тривиальном C. И никаких template тут не нужно!
[00:32:50] <ada_ru> (vasil_sd) отвечает (sergey_dukov) на <Да нет. Задание бито…>
Нет, сишнику до ады далеко.
[00:33:34] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Интересно. А есть сс…>
https://www.youtube.com/watch?v=8tG4LawDYI8
https://arxiv.org/pdf/1901.10220.pdf
[00:34:00] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <https://www.youtube.…>
Отлично! Спасибо!
[00:34:47] <ada_ru> (I_vlxy_I) это reproduction study. то есть была нашумевшая статья которая офигенную разницу нашла. а тут попробовали воспроизвести и проанализировать результаты. очень познавательно.
[00:34:58] <ada_ru> (I_vlxy_I) плюс мелкое свое исследование провели
[00:36:05] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <это reproduction stu…>
Ага, уже смотрю.
Если есть ещё что-либо из похожего, то буду благодарен.
[00:36:13] <ada_ru> (I_vlxy_I) жаль что подобным сейчас почти перестали заниматься 🙁 вокруг кричат про методологии модные которые скорость разработки увеличивают, качество кода повышают и так далее, но четких и воспроизводимых результатов экспериментов и статей - нет.
[00:36:33] <ada_ru> (I_vlxy_I) программирование скатывается в совсем уж гуманитарщину с модой и вкусовщиной.
[00:36:40] <ada_ru> (Oleg) отвечает (sergey_dukov) на <Да нет. Задание бито…>
В Си будет разница в BigEndian/LitleEndian
[00:37:46] <ada_ru> (sergey_dukov) отвечает (vasil_sd) на <Нет, сишнику до ады …>
Ну насчёт писанины, — вопрос спорный. На АДЕ обычно писанины больше. Премущество С — локаничность, некотовые это любят другие ненавидят.
[00:37:51] <ada_ru> (Oleg) отвечает (I_vlxy_I) на <программирование ска…>
И ещё скоро надо будет индийский паспорт, чтоб устроится на работу программистом :-)
[00:38:21] <ada_ru> (I_vlxy_I) отвечает (Oleg) на <И ещё скоро надо буд…>
не, чтобы устроиться менеджером в программерской конторе. для того, чтобы быть программистом - китайский нужен.
[00:38:40] <ada_ru> (vasil_sd) отвечает (sergey_dukov) на <Ну насчёт писанины, …>
Я когда-то ненавидел паскаль из-за verbosity. Потом повзрослел, поработал и понял, что лаконичность - это на последнем месте.
[00:38:54] <ada_ru> (Oleg) отвечает (sergey_dukov) на <Ну насчёт писанины, …>
Для меня у Си только одно преимущество - он везде поддерживается , и он очень прозрачен для понимания
[00:39:04] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <программирование ска…>
Уже там и весьма давно
[00:39:55] <ada_ru> (vasil_sd) отвечает (Oleg) на <Для меня у Си только…>
Особенно указатели на функции, которые принимают и возвращают указатели на функции :)))
[00:40:54] <ada_ru> (Oleg) отвечает (vasil_sd) на <Особенно определение…>
Ну после ассемблера вполне прозрачно :-)
[00:41:16] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Уже там и весьма дав…>
последние попытки поставить серьезный эксперимент по сравнению надежности ЯП и поизводительности программистов - это конец 90-х начало 2000х. с тех пор больше ничем таким не занимались, кажется. 🙁
сейчас вот стало модно шерстить github и пытаться проанализировать то, что напарсил. но результаты получаются, мягко говоря, не шибко чистыми.
[00:41:21] <ada_ru> (sergey_dukov) Я предрочитаю АДУ с её писаниной. Пускай писанины больше, всё становится более понятным, и больше вероятность того, что программа будет работать правильно.
[00:41:34] <ada_ru> (vasil_sd) отвечает (Oleg) на <Ну после ассемблера …>
Да уж. Я когда-то под Win32 на tasm'e писал... :)))
[00:43:04] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <последние попытки по…>
Так там много параметров и не видно.
Например: стоимость ошибок, стоимость поддержки и пр. (стоимость в широком смысле: время, деньги и тд)
[00:44:45] <ada_ru> (I_vlxy_I) но это не значит что надо совсем уж забить на все и область принятия решений полностью отдать на откуп маркетологам
[00:45:22] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <последние попытки по…>
Кроме того, тут тяжело ввести хорошие метрики, чтобы всё это достоверно померять. Всё будет очень субъективно.
Даже вопрос производительности программистов весьма и весьма нетривиальный.
[00:45:40] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Кроме того, тут тяже…>
я знаю 🙁
[00:46:29] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <но это не значит что…>
Так уже. Вон последние события вокруг 737MAX. Когда боинг нанимал аутсорсеров, ибо дешевле и пудрил мозги контроллирующим органам....
[00:46:41] <ada_ru> (sergey_dukov) отвечает (vasil_sd) на <Да уж. Я когда-то по…>
Вот это по настоящему переносимые программы. Запускаются в Windows любой версии!
[00:46:56] <ada_ru> (Oleg) https://www.google.ru/amp/s/amp.rbc.ru/rbcnews/business/10/01/2020/5e180ab19a794778166d3bd8
[00:47:01] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Так уже. Вон последн…>
дык аутсорсеры то не факт что виноваты. да и деньги они вполне ок получали.
[00:47:09] <ada_ru> (Oleg) Вот такие программисты ...
[00:48:00] <ada_ru> (Oleg) Только по-моему 737 MAX до аутсорсинга как раз был сделан
[00:48:13] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <дык аутсорсеры то не…>
Там инженеры боинга где-то по форумам весьма нелестно об этих аутсорсерах отзывались. Когда начальство заставляло делать приёмку кривого софта.
[00:48:47] <ada_ru> (I_vlxy_I) про аутсорсеров (которые отнимают рабочие места у тебя) редко кто хорошо отзывается 🙂
[00:48:55] <ada_ru> (I_vlxy_I) они вообще - чужие и чуждые
[00:49:10] <ada_ru> (Oleg) Да там проблема то не в софте а в том что самолёт в целом говно
[00:49:22] <ada_ru> (Oleg) Без софта летать не может
[00:49:31] <ada_ru> (Oleg) Двигатели так расположены
[00:49:35] <ada_ru> (vasil_sd) отвечает (Oleg) на <Только по-моему 737 …>
Я уже деталей не помню, но тот блок, который корректирует момент кручения от движков писали то ли индусы то ли ещё кто-то через фирму-прокладку.
А на инженеров боинга давили, чтобы они это принимали.
[00:50:11] <ada_ru> (I_vlxy_I) Хуяк-хуяк и в прод!
[00:50:20] <ada_ru> (Oleg) А может просто не надо было такие двигатели и так вешать?
[00:50:25] <ada_ru> (vasil_sd) отвечает (Oleg) на <Да там проблема то н…>
Ну и это тоже.
[00:51:05] <ada_ru> (vasil_sd) отвечает (Oleg) на <А может просто не на…>
А они не могли по-другому. Там движки большие. В общем, хотели денег быстро и с минимумом усилий...
[00:51:30] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Хуяк-хуяк и в прод!>
Весь бизнес сейчас так, увы :(
[00:51:36] <ada_ru> (I_vlxy_I) я читал развернутую статью про то, как в гражданский боинг пришло руководство из военного боинга и после этого культура инженерии стала угасать в Боинге.
[00:51:41] <ada_ru> (Oleg) Это все айрбас виноват - он раньше выкатил свой лайнер , а Боингу пришлось так делать
[00:51:56] <ada_ru> (Oleg) Надо оштрафовать айрбас :-)))
[00:51:58] <ada_ru> (I_vlxy_I) ибо военка привыкла больше пилить и меньше за инженерией следить
[00:52:11] <ada_ru> (vasil_sd) отвечает (Oleg) на <Надо оштрафовать айр…>
Санкции, санкции :))
[00:52:42] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <ибо военка привыкла …>
Вот тут не знаю. Про военку прямо противоположное читал от кого-то из локхида
[00:55:10] <ada_ru> (Oleg) отвечает (vasil_sd) на <Вот тут не знаю. Про…>
Локхид те ещё красавцы
[00:57:04] <ada_ru> (Oleg) Они там термоядерный реактор обещали компактный лет 5 назад
[00:57:40] <ada_ru> (vasil_sd) отвечает (Oleg) на <Локхид те ещё красав…>
К сожеалению не смог быстро найти ту ветку. Там человек из локхида сказал, что у них почти одинаковые движки разрабатывались для военки и для гражданки.
Для военки они кодили на Аде под присмотром военных, для гражданки сишник/плюсы. Так по его словам, на военную авионику ушло в два раза меньше времени при почти в два раза меньшем количестве людей. И отладили её быстро. А гражданский вариант - долго до ума доводили
[00:58:32] <ada_ru> (Oleg) https://www.lockheedmartin.com/en-us/products/compact-fusion.html
[00:58:41] <ada_ru> (Oleg) Во, где ? Дайте два
[00:58:48] <ada_ru> (Oleg) А нету .... :-(
[00:58:51] <ada_ru> (vasil_sd) отвечает (Oleg) на <Они там термоядерный…>
Ну да. Сейчас СССР нету, можно бюджеты пилить пол любыми лозунгами в любых объемах :))
[00:59:37] <ada_ru> (Oleg) Причём эту ловушку в СССР рассматривали много лет назад и отказались
[01:00:55] <ada_ru> (I_vlxy_I) отвечает (Oleg) на <Причём эту ловушку в…>
отказались от СССР? 🙂
[01:01:22] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <отказались от СССР? …>
Это мы отказались, а они радовались этому :))
[01:03:16] <ada_ru> (vasil_sd) отвечает (Oleg) на <Причём эту ловушку в…>
Я где-то слышал мнение, что ловушка нормальная возможно только гравитационная. От которой можно выход получить больше единицы.
[01:03:30] <ada_ru> (I_vlxy_I) "military procurement and engineering created a corrupt design process, with unnecessary complexity, poor safety standards"
[01:03:34] <ada_ru> (I_vlxy_I) https://mattstoller.substack.com/p/the-coming-boeing-bailout
[01:03:38] <ada_ru> (I_vlxy_I) вот, нашел статью
[01:04:15] <ada_ru> (Oleg) отвечает (vasil_sd) на <Я где-то слышал мнен…>
Возможно. Вот скоро ITER достроят и узнаем
[01:04:47] <ada_ru> (I_vlxy_I) "Military contractors subcontract based on political concerns, not engineering ones. If contractors need to influence a Senator from Montana, they will place production of a component in Montana, even if no one in the state can do the work."
[01:04:58] <ada_ru> (vasil_sd) отвечает (Oleg) на <Возможно. Вот скоро …>
Если раньше бюджеты не попилят и не утащат :)))
Сейчас коррупция даже до учёных добралась 😩
[01:06:10] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <"Military contractor…>
Классика. Меня как технаря очень бесит, когда в технических проектах принимаются политические решения
[01:23:42] <ada_ru> (Gourytch) отвечает (I_vlxy_I) на <а вот @Gourytch и се…>
Не.я сейчас только собираюсь на работу. Мне еще девять часов до неё ехать-лететь
[01:24:05] <ada_ru> (I_vlxy_I) отвечает (Gourytch) на <Не.я сейчас только с…>
на такси лететь? 🙂
[01:24:14] <ada_ru> (I_vlxy_I) вроде в москве обещали, что это будет возможно!
[01:24:31] <ada_ru> (Gourytch) ехать на таксях а лететь на ерофлоте
[01:25:04] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <вроде в москве обеща…>
Ещё немного - и единственный способ перемещения по Москве будет только по воздуху :)
[01:25:05] <ada_ru> (I_vlxy_I) яндекс.самолёт
[01:25:08] <ada_ru> (I_vlxy_I) яндекс.танк!
[01:25:42] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Ещё немного - и един…>
нужно срочно делать систему катапульт! идеальный транспорт!
[01:26:34] <ada_ru> (Gourytch) Яндекс.телепорт )
[01:29:38] <ada_ru> (vasil_sd) отвечает (Gourytch) на <Яндекс.телепорт )>
Ой, я бы ни за что не стал пользоваться :)))
Работая в Яндексе и зная, как здесь ведётся разработка :)))
Телепортируют как-нить неправильно, а потом "ну извиняйте, вот вам бонусов на Беру, как компенсация за третье ухо и отсутствующую ногу"
[01:31:54] <ada_ru> (zloidemon) отвечает (vasil_sd) на <Ой, я бы ни за что н…>
Бизнес жеж =)
[01:31:56] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Ой, я бы ни за что н…>
да ладно, выкатить на 1% пользователей, если что не так - откатим!
[01:32:05] <ada_ru> (I_vlxy_I) ну а если совсем чутка пятисотить будет телепорт, то и не страшно
[01:32:10] <ada_ru> (zloidemon) Ну да, АБ тесты все дела
[01:32:28] <ada_ru> (zloidemon) Я когда ещё в RTB рекламе работал, мы на часть пользователей всегда выкатывали, а не сразу
[01:33:53] <ada_ru> (I_vlxy_I) отвечает (zloidemon) на <Я когда ещё в RTB ре…>
дык это везде так, где онлайн сервисы. ну, почти везде 🙂 где немного успели подумать мозгом и реализовать такую возможность
[01:34:13] <ada_ru> (I_vlxy_I) надо в Боинг эту идею продвинуть!
[01:34:43] <ada_ru> (zloidemon) отвечает (I_vlxy_I) на <дык это везде так, г…>
Не знаю даже, я больше в больших конторах не работал. Хотя сейчас один из клиентов уже стал большой конторой, а я и не заметил как
[01:35:28] <ada_ru> (I_vlxy_I) я читал про booking.com - там также. причем даже еще экстремальней. они вообще одно время не тестировали - сразу в прод на процент пользователей и смотрели метрики
[01:36:23] <ada_ru> (zloidemon) отвечает (I_vlxy_I) на <я читал про booking.…>
Вот кстати АБ тестирование с всякими CI/CD не особо по смыслу сходится с тем что в книгах пишут. И всё это тестирование больше похоже на то, что у тебя код тестами не весь покрыт и надо на живых данных проверить.
[01:36:52] <ada_ru> (zloidemon) Если брать книжки, и как пишут про CD, то надо лить после тестов сразу на прод, но это какая-то грань фантастики
[01:37:03] <ada_ru> (I_vlxy_I) дык код то у тебя может быть просто огонь и без ошибок, но гипотеза в бизнес области может быть не верна
[01:37:35] <ada_ru> (I_vlxy_I) отвечает (zloidemon) на <Если брать книжки, и…>
ну вот в букинге вроде бы даже без тестов сразу лили 🙂 может юниттесты были, я не помню уже
[01:37:40] <ada_ru> (zloidemon) Угу, поэтому все эти CI/CD теряют смысл, и валится как карточный домик на реальных бабках, а не на сайтах с котиками
[01:38:37] <ada_ru> (I_vlxy_I) ну, CI/CD дает какую-то гарантию что код у тебя более-менее целостный, и позволяет автоматом в прод (или в тест-прод) выкатить. то есть по сути - автоматизаци рутины.
[01:38:54] <ada_ru> (I_vlxy_I) а уж что у тебя там с точки зрения смысловой нагрузки, то такоэ...
[01:39:36] <ada_ru> (zloidemon) отвечает (I_vlxy_I) на <ну, CI/CD дает какую…>
Да, но всё же если есть деньги или прямая связь на них, то лучше АБ делать, даже если у тебя куча тестов и прочего
[01:40:05] <ada_ru> (I_vlxy_I) ну да. гипотезы то относительно пользователей (если у тебя они есть) иначе и не проверишь
[01:41:10] <ada_ru> (zloidemon) А вот типа боинга, там если честно я не знаю даже как бы правильно было всё это тестировать. Ощущение складывается что там на каждый чих пых должен быть тест. Ибо тест АБ ты там не сделаешь, в случае провала это смерть
[01:42:44] <ada_ru> (I_vlxy_I) ну, смерть может наступить и из за заглючившего яндекс.навигатора, так то.
[01:43:32] <ada_ru> (zloidemon) Хорошо что напомнил про навигатор, сейчас сделаю репорт в мапс.ме =)
[01:43:56] <ada_ru> (I_vlxy_I) а что там mail.ru накосячил? 🙂
[01:45:34] <ada_ru> (zloidemon) отвечает (I_vlxy_I) на <а что там mail.ru на…>
Ошибка в коде у них, если допустим отрубить maps.me сеть, и увеличить область где карты нет, то будет пытаться скачать её. Потом закрываешь приложение, и открываешь снова, и оно падает. Не обрабатывают исключения, что доступа к сети нет на андроиде при загрузке карт.
[01:47:47] <ada_ru> (I_vlxy_I) хех
[01:48:16] <ada_ru> (I_vlxy_I) интересно, они своих таксистов уже пересадили на maps.me, или еще нет?
[01:49:51] <ada_ru> (zloidemon) Там же по сути отдельная контора, citymobile или как-то так. У них там всё своё.
[01:50:08] <ada_ru> (zloidemon) Это же не яндекс, который строит монополию
[01:51:27] <ada_ru> (I_vlxy_I) отвечает (zloidemon) на <Там же по сути отдел…>
неа. в смысле для ситимобила они что-то пытаются аутсорсить, но также у них есть корпоративный сервис на базе maps.me и они его развивают прежде всего для своих нужд - для дилевериклаба и для ситимобила
[01:52:57] <ada_ru> (I_vlxy_I) если что, яндекс.такси тоже не яндекс пилит, а отдельная компания 🙂
[01:53:01] <ada_ru> (zloidemon) отвечает (I_vlxy_I) на <неа. в смысле для си…>
Не знаю, может и так, а может и нет. Даже если они и делают это, то в любом случае хорошо. Мне maps.me нравится, очень хороший продукт если допусти за пределы РФ выезжаешь. В пределах РФ пока что альтернативы 2gis не существует, все эти yandex карты и даже maps.me уровень мусора
[01:53:18] <ada_ru> (I_vlxy_I) яндекс карты хороши в москве
[01:53:22] <ada_ru> (I_vlxy_I) не в москве - такоэ
[01:54:17] <ada_ru> (zloidemon) Из-за пробок?
[01:55:01] <ada_ru> (I_vlxy_I) отвечает (zloidemon) на <Из-за пробок?>
и пробки и карта довольно актуальная. панорамы есть всего и вся.
за пределами москвы в плане панорам какой-нибудь гугл уже лучше
[01:55:45] <ada_ru> (zloidemon) отвечает (I_vlxy_I) на <и пробки и карта дов…>
У меня обычно задача - посмотреть маршруты транспорта, либо найти кафешку. Так что и 2gis хватает за глаза
[01:56:28] <ada_ru> (I_vlxy_I) у меня в москве - маршруты транспорта, текущее расположение транспорта, парковки, проложить маршрут через несколько видов транспорта. пробки, перекрытия
[01:56:58] <ada_ru> (I_vlxy_I) а панорамы - везде нужны, для любого места где я не был. чтобы представлять что я должен увидеть когда буду в окрестностях цели
[01:58:23] <ada_ru> (zloidemon) Понятно, но в любом случае хорошо когда есть конкурирующие продукты. Но так как я с Сибири приехал в МСК, у меня всё же остались привычка использовать 2gis. Пробок только нет, а так без онлайна даже вполне себе годно работает.
[01:59:09] <ada_ru> (I_vlxy_I) да, хорошо когда есть несколько конкурентов
[02:01:03] <ada_ru> (zloidemon) отвечает (I_vlxy_I) на <да, хорошо когда ест…>
Это точно, у меня вот такое ощущение что в том же ЕС отстало в этом плане. У них кроме гугла ничего и не работает, и тот же maps.me это опять же оффлан карты без всяких ништяков.
[02:01:44] <ada_ru> (I_vlxy_I) А OsmAndMaps?
[02:01:56] <ada_ru> (I_vlxy_I) Waze (или это гугл?)
[02:02:02] <ada_ru> (I_vlxy_I) гармин какой
[02:02:32] <ada_ru> (I_vlxy_I) bing maps
[02:02:35] <ada_ru> (zloidemon) Сейчас гляну, я про аналоги 2gis где юрлица есть имею ввиду. Что бы кафешки удобно искать с телефонами и тд
[02:03:06] <ada_ru> (zloidemon) Без того что бы заходить в гугл и в поиске вбивать, а поставить например ПО приехать и не заморачиваться с роумингом, интернетом и тд и тп.
[02:05:10] <ada_ru> (I_vlxy_I) кафешки это ж yelp
[02:09:42] <ada_ru> (zloidemon) Спасибо, запишу, про некоторые из списка ранее вообще не слышал.
[02:14:33] <ada_ru> (Gourytch) Буду наслаждаться красотами до утра... https://www.ada-ru.org/files/bot/2020-01-12-x5.jpg
[02:18:02] <ada_ru> (I_vlxy_I) отвечает (Gourytch) на <>
гм. задерживают вылет?
[02:19:27] <ada_ru> (Gourytch) отвечает (I_vlxy_I) на <гм. задерживают выле…>
Нет. Всё вовремя. Просто вылет в 6:15 по GMT+5
[02:20:05] <ada_ru> (I_vlxy_I) хех. это ж бесчеловечно после такого в понедельник идти такси ковырять
[02:20:24] <ada_ru> (Gourytch) Таски такси )
[02:22:22] <ada_ru> (Gourytch) Я бы отоспался, но фигу: сегодня еще по проекту совещания. Буду тупо пялиться в проекции морквичей на экран и пытаться распарсить знакомые фразы.
[02:24:49] <ada_ru> (I_vlxy_I) отвечает (Gourytch) на <Я бы отоспался, но ф…>
ну у вас хотя бы примерно на русском 🙂 суровей когда в таком состоянии на совещалове с коллегами на инглиш лангуяге 🙂
[02:25:14] <ada_ru> (I_vlxy_I) парселке совсем туго в такие моменты
[02:26:28] <ada_ru> (Gourytch) отвечает (I_vlxy_I) на <ну у вас хотя бы при…>
есть ещё более страшное: когда английский с характерным индийским говором )
[02:26:39] <ada_ru> (I_vlxy_I) о, да!
[02:28:59] <ada_ru> (Gourytch) Если б не тындекс - слушал бы я его сейчас... или раньше кукухой бы поехал. Пушо что индусу ок, то неиндусу не ок )
[02:30:38] <ada_ru> (I_vlxy_I) яндекс.такси спасает людей!
[02:34:49] <ada_ru> (Gourytch) Это да )
[03:26:33] <ada_ru> (Oleg) отвечает (I_vlxy_I) на <Waze (или это гугл?)>
Они п.....сы убрали поддержку Pioneer AppRadio зачем то
[03:32:32] <ada_ru> (Oleg) Аэропорт Курчатов это ж Челябинск :-)
[04:09:58] <ada_ru> (Gourytch) отвечает (Oleg) на <Аэропорт Курчатов эт…>
Угу
[04:48:14] <ada_ru> (sergey_dukov) Что то [ada_ru] не передаёт вложения, передаю для Васила.
[04:48:16] <ada_ru> (sergey_dukov) <прислал документ>
[09:15:21] <ada_ru> (vasil_sd) отвечает (sergey_dukov) на <Что то [ada_ru] не п…>
Спасибо!
Сейчас посмотрю
[09:23:20] <ada_ru> (vasil_sd) отвечает (sergey_dukov) на <Что то [ada_ru] не п…>
Всё-равно не догоняю.
Перенос "+" в параметры P напрямую меняет смысл кода. S - это чистый сигнатурный пакет, для того, чтобы параметры пачкой таскать.
Основной вопрос в том, почему есть разница в use type перед функцией на уровне пакета и в определении самой функции. Смотрел у Барнса, смотрел стандарт, про области видимости, про инстанциацию дженериков, но так и не понял, в чём разница. Почему в одном случае компилятор нормально добавляет "+" в область видимости, а во втором - не хочет. По идее область видимости в определении функции является расширением области видимости пакета и 'use type' там должно тоже так же работать. В определении функции мы же тоже так же видим этот S_inst?
[09:32:00] <ada_ru> (vasil_sd) отвечает (sergey_dukov) на <Что то [ada_ru] не п…>
Прочитал комментарий на ada-ru. Вроде бы что-то начинаю понимать, но ещё смутно. S_ins.T есть же уже в области видимости до функции, оно же из параметров приехало? как 'use type ...' определяет тип? Это же просто для затаскивания операторов, связанных с типом в область видимости? И в теле функции если использовать S_inst."+" то всё норм. То есть в теле функции виден и тип S_inst.T и операторы к нему, без uset type на уровне пакета
[09:56:26] <ada_ru> (Oleg) https://m.youtube.com/watch?v=gKEOzRm7aaw
[09:57:10] <ada_ru> (Oleg) Что-то я не понимаю , как такие ошибки верификации вобще допускаются
[09:58:45] <ada_ru> (vasil_sd) отвечает (Oleg) на <Что-то я не понимаю …>
А там про что? Acsl + frama-c?
[09:59:48] <ada_ru> (Oleg) Мне непонятно как при ошибке которая в итоге даёт условие и отрицание функция верификацируется
[10:00:02] <ada_ru> (Oleg) Сейчас скажу на какой минуте
[10:01:20] <ada_ru> (Oleg) 40:20
[10:01:37] <ada_ru> (Oleg) Там по AdaCore прошлись тоже :-)
[10:02:12] <ada_ru> (vasil_sd) У frama-c с acsl есть фундаментальная проблема: сишник не имеет формальной операционной семантики, поэтому отверифицировать можно на 100% и получить нерабочий код с багами...
[10:02:43] <ada_ru> (vasil_sd) отвечает (Oleg) на <40:20>
Ок, как доберусь до хорошего инета, посмотрю
[10:03:52] <ada_ru> (vasil_sd) отвечает (Oleg) на <Там по AdaCore прошл…>
А вот это уже интереснее, учитывая то, что для спарка вроде есть формальная операционная семантика
[10:04:25] <ada_ru> (Oleg) Ну там вспомнили о какой то древней проблеме
[10:04:36] <ada_ru> (Oleg) Но если честно доклад так себе
[10:10:08] <ada_ru> (vasil_sd) Глянул кадры, там указатель +1, тут нужно внимательно смотреть, как это странслировалось в why3 и что там с интами и сепарационной логикой
[10:13:44] <ada_ru> (vasil_sd) При трансляции в why3 косяков хватает, я сам когда-то репортил в adacore относительно ошибок в трансляции gnatprove.
[10:14:14] <ada_ru> (Eugene) если не определена формальная семантика, то и верифицировать нечего
[10:15:48] <ada_ru> (vasil_sd) отвечает (Eugene) на <если не определена ф…>
Ну как бы frama-c с плагинами неявно её какую-то определяют, но по факту с компиляторными точками зрения расхождения есть и иногда существенные
[10:27:22] <ada_ru> (vasil_sd) отвечает (sergey_dukov) на <Что то [ada_ru] не п…>
Посмотрел всё внимательно, всё равно не понимаю.
Если внутри функции вместо use type S_Inst.T сделать просто use S_inst, то всё нормально приезжает в область видимости, и T и +. То есть, тут получается без разницы где писать use, на уровне пакета или в определении функции, а вот с use type разница есть, хотя вроде бы не должно быть.
[10:32:42] <ada_ru> (vasil_sd) отвечает (vasil_sd) на <Посмотрел всё внимат…>
ARM2012 8.4 уже несколько раз медленно перечитал, всё-равно не понятно, почему для компилятора есть разница, в том где находится 'use type'.
[11:48:39] <ada_ru> (iserged) отвечает (I_vlxy_I) на <о! хочу предсказание…>
Конечно, это будет rustRustRUST... с третьей-то итерации
[11:50:19] <ada_ru> (I_vlxy_I) отвечает (iserged) на <Конечно, это будет r…>
А если со второй, а Ада третья?
[11:51:34] <ada_ru> (I_vlxy_I) А если Ада и Раст будут параллельно писаться? :-) по этапам. И то Ада будет впереди то Раст в плане прогресса выполнения задачи.
[11:54:43] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <А если Ада и Раст бу…>
Тут зависит от того, на чём программист застрянет сильнее: барьер входа в язык или перевод задачи на новые идиомы и писанина.
И небольшая задача совсем нерепрезентативна (да и один программист тоже) для анализа.
[11:55:41] <ada_ru> (vasil_sd) По моему наблюдению, плюсовики в Аду въезжают быстрее, но их отталкивает verbosity.
[11:58:00] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <По моему наблюдению,…>
Это похоже на отношение к Го у плюсовиков
[11:58:14] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Это похоже на отноше…>
Да, примерно.
[11:58:22] <ada_ru> (iserged) отвечает (I_vlxy_I) на <А если со второй, а …>
при входных условиях, что программист одинаково владеет средствами разработки, и работает по одному и тому же тз, то каждая последующая итерация дается проще. Ну при условии, что инструментарий предоставляет необходимые примитивы и не приходится для того, чтобы реализовать тз, сначала реализовать кучу технокалия
[11:58:37] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Да, примерно.>
Но хоть дженерики есть и исключения :-)
[11:59:17] <ada_ru> (I_vlxy_I) отвечает (iserged) на <при входных условиях…>
У задачи нет зависимостей. Даже стандартная либа не особо нужна
[12:01:13] <ada_ru> (I_vlxy_I) А вот что там и сям с IDE это хз :-)
[12:01:17] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <У задачи нет зависим…>
Тут вопрос в области, откуда задача. Если она хорошо ложиться на обычное структурное программирование, то у Ады хорошие шансы.
Из ООП думаю тоже.
Если задача из числодробительных, то тут, кмк, раст будет впереди
[12:01:23] <ada_ru> (iserged) отвечает (I_vlxy_I) на <У задачи нет зависим…>
Ну смотри, мы же говорим не о гарантиях, а о реализации. Даже о скорости реализации одного и того же. Поэтому я и говорю, что каждая итерация дает нам некоторые преимущества.
[12:02:35] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Тут вопрос в области…>
А что у числодробилок? Если нет жестких требований к произодиьельности, то на Аде алгоритмы такие вроде просто пишутся
[12:03:04] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <А что у числодробило…>
Там меньше завязка на абстракции языка и можно тупо быстрее закодить
[12:03:17] <ada_ru> (I_vlxy_I) отвечает (iserged) на <Ну смотри, мы же гов…>
Поэтому я и написал про смешанную итерацию - когда параллельно пишется
[12:04:24] <ada_ru> (Oleg) А я пришел к выводу что ну его нахрен, ограничусь C/C++/ADA/Go/Python
[12:04:51] <ada_ru> (vasil_sd) отвечает (Oleg) на <А я пришел к выводу …>
Вот, кстати, показательно про барьер раста
[12:04:52] <ada_ru> (Oleg) Вот еще тут немного с Perl копался 😊 бедные люди....
[12:05:38] <ada_ru> (Oleg) отвечает (vasil_sd) на <Вот, кстати, показат…>
Нет там никакого барьера, не хочу просто тратить время не получив сильно важное в замен
[12:06:19] <ada_ru> (Oleg) Барьер - это например "Квантовые поля" там да, надо много знать чтоб начать чтото понимать
[12:06:38] <ada_ru> (vasil_sd) отвечает (Oleg) на <Нет там никакого бар…>
Если бы не было барьера, то было бы C/c++/ada/rust/go
[12:07:04] <ada_ru> (Oleg) отвечает (vasil_sd) на <Если бы не было барь…>
Я пока не оценил его видимо
[12:07:19] <ada_ru> (Oleg) В моей области пока неочевидные плюсы
[12:07:45] <ada_ru> (Oleg) То есть замена Go в простых проектах не дает скорости ни кода ни времени разработки
[12:08:06] <ada_ru> (vasil_sd) отвечает (Oleg) на <Нет там никакого бар…>
Раст на самом деле по многим параметрам очень интересный язык.
При производительности сишника можно получить безопасность близкую к Аде
[12:08:17] <ada_ru> (Oleg) Согласен
[12:08:40] <ada_ru> (Oleg) Но только пока нет широкой поддержки как у C/C++
[12:08:43] <ada_ru> (Gourytch) картинка https://www.ada-ru.org/files/bot/2020-01-13-x6.jpg
[12:09:04] <ada_ru> (vasil_sd) отвечает (Oleg) на <То есть замена Go в …>
Ну тут зависит от области проекта.
[12:09:43] <ada_ru> (Oleg) отвечает (vasil_sd) на <Ну тут зависит от об…>
Так я и говорю - изучив ситуацию со своими областями - пока нет выгоды - только потеря времени
[12:10:07] <ada_ru> (Oleg) Увы пока и C особо заменить кое где не чем и даже ADA/SPARK не вариант
[12:10:34] <ada_ru> (Oleg) Кстати AdaCore там чтото про широкую поддержку vxworks писали
[12:11:15] <ada_ru> (Oleg) отвечает (Gourytch) на <>
😊
[12:14:10] <ada_ru> (Максим) отвечает (Oleg) на <Кстати AdaCore там ч…>
Да в АдаКоре с vxworks всё хорошо, кажется
[12:15:17] <ada_ru> (iserged) отвечает (I_vlxy_I) на <Поэтому я и написал …>
Ну это странно. Можно сказать, на котором яп он напишет последнюю строчку, тот и проиграл))) если ты имеешь ввиду, что где-то писанины больше, в плане procedure, proc, fn.. и он быстрее запишеь там, где тупо кейворды короче, идентификаторы короче... то я думаю, что нет. Я не вижу особой корреляции между длиной/ количеством кейвордов и скорости разработки, а короткие маловразумительные идентификаторы, скорее всего, сн дят скорость разработки, так как контекст определения будет где- то в другом месте, и придется вспоминать что означает bla, blabla, blablabla или скакать по коду. В общем, если отбросить индивидуальности, и учесть, что программист одинаково владеет используемым инструментарием, о быстрее он напишет на языке, который ему более приятен
[12:18:04] <ada_ru> (Oleg) Твою ж мать
[12:18:11] <ada_ru> (Oleg) Support for Modern Development Languages, Frameworks, and Infrastructures
C11, C++14, and C++17
Python
Rust
Boost
LLVM
[12:18:22] <ada_ru> (Oleg) Это на WindRiver про VXWorks
[12:18:52] <ada_ru> (Oleg) Rust есть ADA нет....... ну то есть она есть но почему нет в титульной странице
[12:19:31] <ada_ru> (Oleg) Понятно что Modern это не ADA 😊 но C11 это тоже так себе Modern
[12:21:42] <ada_ru> (iserged) <прислал запись>
[12:22:11] <ada_ru> (Oleg) отвечает (iserged) на <>
Послание от пришельцев 😊))
[13:00:10] <ada_ru> (I_vlxy_I) отвечает (iserged) на <Ну это странно. Можн…>
Нет, не так. Делается замер времени на каждый этап на каждом ЯП. Время потом суммируется по всем этапам. Не важно какой ЯП был первым, а какой последним.
[13:03:43] <ada_ru> (iserged) отвечает (I_vlxy_I) на <Нет, не так. Делаетс…>
А в какой последовательности выбираются языки на каждом из этапов?
[13:07:59] <ada_ru> (I_vlxy_I) С перекрытием. 2-2 этапа
`RR
AA`
[13:08:24] <ada_ru> (I_vlxy_I) Так
[13:11:16] <ada_ru> (I_vlxy_I) То есть каждый раз делается 2 этапа на каждом ЯП со смещением фазы :-)
[13:12:18] <ada_ru> (I_vlxy_I) отвечает (Oleg) на <Понятно что Modern э…>
Чем Ада-2012 не модерн?
[13:13:02] <ada_ru> (Oleg) Да на самом деле похоже AdaCode в прошлом году только сильно занялся VxWorks
[13:40:28] <ada_ru> (I_vlxy_I) отвечает (iserged) на <А в какой последоват…>
То есть для языков все симметрично выходит.
[13:49:27] <ada_ru> (Максим) Хотите идей про веб дизайн на Аде? Например, вы пишите клиентский код на Аде для обработки какой-то формы. Как развесить обработчики событий?
[13:49:44] <ada_ru> (Максим) Вот подход, который мы использовали в a2js: https://pastebin.com/8YvJpw3j
[13:50:46] <ada_ru> (Максим) А вот как можно было бы, если обыграть идею прерываний на Аде: https://pastebin.com/pdpfx1EU
[14:32:38] <ada_ru> (Максим) Хотя не понятно, где возьмётся лишний (главный) поток управления 😕
[14:43:29] <ada_ru> (I_vlxy_I) Вебворкеры?
[14:44:02] <ada_ru> (I_vlxy_I) Через них в wasm эмулируются pthreads
[14:44:40] <ada_ru> (vasil_sd) отвечает (Максим) на <Вот подход, который …>
Первый вариант по-приятнее.
[15:49:01] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Первый вариант по-пр…>
Вообще, прикольно что в яндексе кто-Адой интересуется :-) ну и, похоже в Москве уже собралось человеков для мини адской встречи. :-)
[15:49:42] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Вообще, прикольно чт…>
Я в Яндексе вообще-то недавно. И адой интересовался задооолго до Яндекса. :)
[15:50:44] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Я в Яндексе вообще-т…>
Это не важно :-)
[15:51:19] <ada_ru> (vasil_sd) Мой основной интерес - это математика и надёжные системы. Ну у всё что вокруг: от всяких логик, до языков и тулов.
В Яндексе, к сожалению, такие не сильно нужны :(
[15:52:01] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Мой основной интерес…>
Кати в прод, а там разберёмся!
[15:52:34] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Кати в прод, а там р…>
Это не самое плохое что я тут встречал :)
[15:55:11] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Это не самое плохое …>
O_O
[15:55:32] <ada_ru> (I_vlxy_I) Пятисотит, и ладно!
[15:55:34] <ada_ru> (Oleg) отвечает (vasil_sd) на <Мой основной интерес…>
Странно... математики ж нужны всем !
[15:56:53] <ada_ru> (vasil_sd) отвечает (Oleg) на <Странно... математик…>
Я не правильный математик, тут нужны в основном спецы по матстату, ML, нейросеткам и пр.
У меня же область - это матлогика, SAT/SMT, модел-чекинг, формальная верификация и пр.
[16:04:39] <ada_ru> (I_vlxy_I) Логика не нужна. Нужны числодробители!
[16:07:15] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Логика не нужна. Нуж…>
Да уж. Хотя весьма легко можно показать, что логика тоже может приносить бабло
[16:08:13] <ada_ru> (iserged) отвечает (I_vlxy_I) на <То есть для языков в…>
В таком случае, результат непредсказуем и упирается даже не в языковые фичи, а в личные предпочтения программиста
[16:09:23] <ada_ru> (I_vlxy_I) отвечает (iserged) на <В таком случае, резу…>
Его личные предпочтения - c++ :-) очевидно же
Ну, то есть, выходит, что существенной разницы между Адой и растом нет.
[16:09:29] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Логика не нужна. Нуж…>
Я вот даже статьи пытаюсь писать, чтобы объяснять, что правильно приготовленная логика может приносить бабло и счастье всем :)
https://habr.com/ru/company/yandex/blog/457810/
[16:11:38] <ada_ru> (I_vlxy_I) отвечает (I_vlxy_I) на <Его личные предпочте…>
Потому как разница между растом и брейнфаком в таком эксперименте будет очевидна и не будет зависит от предпочтений программиста :-)
[16:15:20] <ada_ru> (iserged) отвечает (I_vlxy_I) на <Его личные предпочте…>
Думаю, что от языка здесь все очень слабо зависит, больше человеческий фактор. Я вот целый месяц пишу на языке с русскими ключевыми словами и идентификаторами, и если сначала у меня был постоянный ступор, о сейчас, по прошествии месяца, я могу сказать, что в этом что-то есть)))
[16:16:02] <ada_ru> (iserged) отвечает (I_vlxy_I) на <Потому как разница м…>
Ну так речь о сравнимых языках, да
[16:21:21] <ada_ru> (Максим) отвечает (iserged) на <Думаю, что от языка …>
type Время is (Прошедшее, Настоящее, Будущее);
type Hаклонение is (Обычное, Повелительное, Сослогательное);
type Число is (Единственное, Множественное);
type Род is (Общий, Мужской, Женский, Средний);
type Падеж is
(Именительный, -- кто? что?
Родительный, -- кого? чего? откуда?
[16:22:41] <ada_ru> (I_vlxy_I) отвечает (iserged) на <Думаю, что от языка …>
Замена лексем мало что даёт. Язык то тем же остаётся по сути.
[16:23:31] <ada_ru> (I_vlxy_I) Но вообще, программисту важна связка языка, компилятора и других тулзов которые он использует при программировании. И в логической согласованности этого всего.
[16:24:01] <ada_ru> (iserged) отвечает (Максим) на <type Время is (Проше…>
Микс выглядит жутка - ключевые слова и идентификаторы должны быть на одном языке
[16:24:30] <ada_ru> (Максим) Зато Ада!
[16:30:31] <ada_ru> (I_vlxy_I) Например очень важно качество диагностики ошибок (и рантайма и компилятора). И чтобы было понятно и по делу написано.
[16:33:36] <ada_ru> (Максим) Вот вам демо на wasm от Вадима! https://www.ada-ru.org/files/wasm/index.html
[16:35:35] <ada_ru> (Vinpuh) отвечает (Максим) на <Вот вам демо на wasm…>
<прислал наклейку> 👍
[16:37:50] <ada_ru> (I_vlxy_I) отвечает (Максим) на <Вот вам демо на wasm…>
<прислал наклейку> 👍
[16:38:12] <ada_ru> (I_vlxy_I) Ада - сила!
[17:03:16] <ada_ru> (Oleg) отвечает (vasil_sd) на <Я вот даже статьи пы…>
О! Verilog VHDL милые душе :-). Статью почитаю. А что в Intel не сложилось ?
[17:07:06] <ada_ru> (vasil_sd) отвечает (Oleg) на <О! Verilog VHDL милы…>
Там проект заглох. такое ощущение, что они наш стартап (Soft Machines Inc) купили для того, чтобы нвидия нас не купила, ну или ещё кто из конкурентов.
Я думал куда-нить в Интеле в верификаторы попробовать, даже разговаривал с Jon Harrison по этому поводу, и даже вроде с женой смог договориться, что если что, поедем в солнечную Калифорнию. Но Интел стали сокращать верификаторов (оптимизация и пр. - пришли новые эфективные менеджеры, видимо) и Джон оттуда уволился. Я подождал ретенш бонуса и тоже пошёл искать лучшее место под луной...
[17:08:43] <ada_ru> (Oleg) Мда.... Интел уже не тот :-)
[17:08:55] <ada_ru> (vasil_sd) отвечает (Oleg) на <О! Verilog VHDL милы…>
Сейчас бывшие коллеги по интелу в основном в nvidia, хуавее и самсунге работают. Там почти весь коллектив разбежался
[17:10:48] <ada_ru> (vasil_sd) отвечает (Oleg) на <Мда.... Интел уже не…>
Да, они как стартанули новую политику continuous transformation, так и всё покатилось.
В плане капитализации конечно молодцы, но технологически - сейчас будут сильно отставать.
Но текущий менеджмент и не парится, типа если что, будем для своих ДЦ и серваков закупать процы у AMD.
[17:11:05] <ada_ru> (Oleg) При этом Intel купил Altera
[17:12:11] <ada_ru> (Oleg) Теперь у меня в приоритете Xilinx / Lattice
[17:12:57] <ada_ru> (vasil_sd) отвечает (Oleg) на <При этом Intel купил…>
Они много чего купили. nervana, например.
И остатки трансметы в своё время тоже.
Тут два момента: накачивать капитализацию и не давать конкурентам покупать слаженные коллективы разработчиков.
Ну, во всяком случае через призму моего опыта.
[17:13:36] <ada_ru> (vasil_sd) То есть, много покупок Интела недружественные и не для развития проектов/технологий.
[17:13:56] <ada_ru> (vasil_sd) В общем, печаль...:(
[17:15:52] <ada_ru> (Oleg) Да все идёт к огромным монополиям
[17:18:17] <ada_ru> (vasil_sd) отвечает (Oleg) на <Да все идёт к огромн…>
Классика, ещё Маркс об этом писал, со времени дедушки Ленина суть не поменялась. Причём монополиям, срастившимся с государством и бюрократией.
[17:35:01] <ada_ru> (I_vlxy_I) Да ладно, Интел всегда периодически проводил массовые сокращения
[17:36:28] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Да ладно, Интел всег…>
Чтобы такие как Харрисон решили уйти, после 20 лет работы, это нужно было сильно постараться (представляете, сколько у него акций, RSU и пр? ).
[17:37:33] <ada_ru> (vasil_sd) Ну, в общем, оттуда сейчас довольно серьёзные спецы поуходили, которые там весьма серьёзными вещами занимались десятки лет.
И это как-то нездоровый признак
[17:39:29] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Да ладно, Интел всег…>
Кстати, а как с Кржаничем поступили? Тоже весьма показательно.
В общем Интел уже не торт :)
[17:40:55] <ada_ru> (I_vlxy_I) Да ладно, зато opencv (точнее itseez) вернули :-)
[17:42:38] <ada_ru> (Oleg) Ну и DPDK
[17:42:47] <ada_ru> (Oleg) Это их
[17:43:50] <ada_ru> (vasil_sd) Тот стартап, в котором я работал примерно такой же путь прошёл. Сначала Мохаммед и Ко отпочковались от Интела, потом через 10 лет Интел обратно купил.
Но видимо нам повезло меньше, ибо целей развивать прокт у Интела, видимо, не было...
[17:46:54] <ada_ru> (I_vlxy_I) Сейчас компьютерное зрение а фаворе..
[17:48:00] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Сейчас компьютерное …>
Это да
[18:00:22] <ada_ru> (I_vlxy_I) https://github.com/ohenley/awesome-ada
[18:14:18] <ada_ru> (Максим) Первый кусок матрешки в alire!
[18:15:13] <ada_ru> (I_vlxy_I) Ура, товарищи!
[18:15:22] <ada_ru> (I_vlxy_I) отвечает (Максим) на <Первый кусок матрешк…>
Ссыль давай!
[18:15:41] <ada_ru> (vasil_sd) отвечает (Максим) на <Первый кусок матрешк…>
Здорово! Нужно будет тоже попробовать
[18:16:35] <ada_ru> (Максим) ~/bin/alr get --build matreshka_league
[18:20:19] <ada_ru> (I_vlxy_I) А на сайте alire где оно?
[18:46:49] <ada_ru> (Максим) а нету! Не обновилось еще, наверное
[20:01:24] <ada_ru> (Максим) https://github.com/RavSS/HAVK
[20:06:51] <ada_ru> (Oleg) О
[20:17:11] <ada_ru> (Oleg) Пошел комп искать 😊
[20:23:27] <ada_ru> (vasil_sd) отвечает (Максим) на <https://github.com/R…>
Интересно, но не увидел спек на основные свойства системы, которые бы доказывались через верификацию.
То есть это - просто минималистичное ядро ос, в котором просто меньше вероятности ошибок времени выполнения из-за буферов и пр.
Оно secure не в том смысле, в котором я изначально подумал (SeL4) :)
[20:24:21] <ada_ru> (I_vlxy_I) Ты очень хардкорное секурити хочешь :-)
[20:25:05] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Ты очень хардкорное …>
Ну, если уж и делать, то только хардкор :) остальное неинтересно :)
[20:27:18] <ada_ru> (vasil_sd) Я тут вспомнил, что на спарке писал когда-то давно и доказывал свойства tlsf аллокатора памяти... Правда не доделал. Думаю выложить, если кому интересно. Может даже руки дойдут доделать...
[20:31:04] <ada_ru> (vasil_sd) Тогда я упёрся в некоторые ограничения возможностей гнатпрува, попробовал подоказывать свойства через драйвер coq, но там наступил на грабли трансляции why3, vcшек в кок, попробовал починить, не получилось и забросил. Попутно ещё пару багов гпрбилда и гнатпрува отрепортил в адакор.
Может сейчас уже эти косяки поправили и можно доделать аллокатор...
[20:31:56] <ada_ru> (vasil_sd) Основная проблема - это формулировка и доказательство свойств высокого уровня поведенческих спек.
[20:33:20] <ada_ru> (vasil_sd) Тогда мне инструменты показались не особо зрелыми для такого рода задач.
Возможно всё уже существенно поменялось
[20:51:29] <ada_ru> (Максим) выкладывай! Для wasm нужен свой аллокатор 😊
[21:01:57] <ada_ru> (vasil_sd) отвечает (Максим) на <выкладывай! Для wasm…>
Ok. По просьбе трудящихся, как откопаю исходники, сразу выложу :)
Попробую в alire :)