[01:44:06] <ada_ru> (I_vlxy_I) казалось бы, при чем тут Rust? https://sun1-83.userapi.com/c849420/v849420692/16a11e/Xz0EtMHuneU.jpg
[10:09:04] <nordwind> Прутья взглядом гнет?
[18:21:55] <ada_ru> (Лекс) отвечает (I_vlxy_I) на <казалось бы, при чем…>
и причём?
[18:30:55] <ada_ru> (Лекс) интересно вот, а почему tensorflow ещё не переписали на rust (ну или на худой конец на го, всё таки гугол же) >_<
[18:35:54] <ada_ru> (I_vlxy_I) отвечает (Лекс) на <интересно вот, а поч…>
а смысл с с++ на го переписывать? тормозить же будет
[18:36:10] <ada_ru> (I_vlxy_I) отвечает (Лекс) на <и причём?>
ржавый кись и ржавый мир!
[18:36:24] <ada_ru> (Лекс) отвечает (I_vlxy_I) на <а смысл с с++ на го …>
ну на раст же) безопасно и быстро
[18:36:47] <ada_ru> (I_vlxy_I) отвечает (Лекс) на <ну на раст же) безоп…>
безопасно но не быстро 😊 пока компилятор раста не столь идеален
[18:37:37] <ada_ru> (Лекс) ой да ладно, там эти доли секунд не играют такой уж решающей роли, это же не реалтайм
[18:38:07] <ada_ru> (I_vlxy_I) доли секунды внутри внутреннего цикла который юзается в обучении? разница может быть в недели в итоге
[18:38:50] <ada_ru> (I_vlxy_I) отработает прога за месяц, или за полтора - это вполне себе разница
[18:39:12] <ada_ru> (Лекс) как-то спорненько, имхо, насчёт недели и месяца
[18:39:44] <ada_ru> (I_vlxy_I) плюс сеточки обученные вполне себе в реалтайме используются.
[18:40:10] <ada_ru> (I_vlxy_I) короче, переписывть - такоэ. можно попутно еще ошибок насажать, которые не про память
[18:41:46] <ada_ru> (Eugene) надо переписать на оберон — сразу сработает магия мэтра Вирта — все ашыпки испарятся )))
[18:42:04] <ada_ru> (I_vlxy_I) отвечает (Eugene) на <надо переписать на о…>
вместе с человечеством! хо-хо-хо!
[19:27:43] <ada_ru> (Лекс) https://github.com/gothinkster/realworld — "The mother of all demo apps" — Exemplary fullstack Medium.com clone powered by React, Angular, Node, Django, and many more medal_sports https://realworld.io/ может кому будет интересно и кто не видел) На аде версии конечно нету, но можно создать issue с просьбой 😃
[22:43:02] <ada_ru> (I_vlxy_I) https://www.linux.org.ru/news/development/15415899
[22:43:06] <ada_ru> (I_vlxy_I) А Ады нету 😞
[22:46:24] <ada_ru> (Лекс) зато есть недолисп на пихоне Hy, недоруби Crystal, непонятно за чем нужный V и не менее стрёмный Red
[22:49:53] <ada_ru> (Лекс) Кстати, коллеги, кто-нибудь мог бы пояснить простым русским языком что такое зависимые типы и для чего они?
[22:54:42] <ada_ru> (Eugene) отвечает (Лекс) на <Кстати, коллеги, кто…>
для того, что бы переложить контроль переполнений с рантайма на компилятор, например.
ну, на самом деле там много чего, в основном для верификации программ...
кстати, есть так называемая Хоаровская теория типов (HTT: Hoare Type Theory), там используются зависимые типы для императивного программирования
[22:55:16] <ada_ru> (Eugene) коротко говоря — зависимые типы позволяют проводить всякие вычисления над типами, и всякое такое
[22:56:36] <ada_ru> (Лекс) я не понимаю как они вообще выглядят, и что означает — вычисления над типами О_О
а в интернете либо сложный матан либо непролазный английский с кучей терминов
[22:56:38] <ada_ru> (Лекс) цитирует (Eugene)
коротко говоря — зависимые типы позволяют проводить всякие вычисления над типами, и всякое такое
[22:57:23] <ada_ru> (I_vlxy_I) Eugene пример давай. Причем такой, чтобы я не смог повторить его на С++ (ведь в нем нет зависимых типов).
[22:57:38] <ada_ru> (Eugene) отвечает (I_vlxy_I) на <Eugene пример давай.…>
да погугли )))
[22:57:54] <ada_ru> (Eugene) если реально, то это всё ещё не на стадии промышленного применения
[22:58:25] <ada_ru> (I_vlxy_I) вроде в Х-е есть (как и всё там - в виде расширизма)
[22:58:44] <ada_ru> (Eugene) отвечает (I_vlxy_I) на <вроде в Х-е есть (ка…>
в хаскель пока не завезли, хотя хаскеллеры с нетерпением ждут
[22:59:03] <ada_ru> (Eugene) отвечает (I_vlxy_I) на <Eugene пример давай.…>
ну вот, сделай сортировку с доказательством корректности
https://github.com/davidfstr/idris-insertion-sort
[23:00:24] <ada_ru> (Лекс) о Господи Иисусе, этот криптованный синтаксис, что там вообще понаписванно и как это читать
[23:00:26] <ada_ru> (Eugene) или вот
https://www.ben-sherman.net/posts/2014-09-20-quicksort-in-idris.html
[23:00:35] <ada_ru> (Eugene) отвечает (Лекс) на <о Господи Иисусе, эт…>
дело привычки же
[23:00:45] <ada_ru> (I_vlxy_I) https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr
[23:00:59] <ada_ru> (I_vlxy_I) пофиг на синтаксис. но объем кода для такой простейшей сортировки доставляет
[23:01:13] <ada_ru> (I_vlxy_I) синтаксис то очень даже ок
[23:01:51] <ada_ru> (Лекс) пофигу та пофигу, только я ничего не понимаю :-( у камлов синтаксис как-то почитабельнее, для не задрота
[23:03:24] <ada_ru> (I_vlxy_I) ты не понимаешь не из за синтаксиса
[23:03:40] <ada_ru> (I_vlxy_I) тут есть понятия в языке которые и я не понимаю. даже близко
[23:04:14] <ada_ru> (Eugene) а вот сделайте доказанную сортировку на спарке ))) что бы там было доказательство того, что выходной массив состоит из тех же элементов, что и входной, но упорядоченных по возрастанию, например ))
[23:06:14] <ada_ru> (I_vlxy_I) доказательство проверяемое компилятором