я просто солидарен с Барухом, не важно, был харассмент или не был, фото не этичное

прекращай

я просто солидарен с Барухом, не важно, был харассмент или не был, фото не этичное

это пиар и только, не надо приставать к людям на фото.

я просто солидарен с Барухом, не важно, был харассмент или не был, фото не этичное

ну зарепорть в инстаграмме, чо скалачат засирать

ну зарепорть в инстаграмме, чо скалачат засирать

там проигнорят, а здесь пока нет.

я такого не читаю к сожалению

http://www.sql.ru/forum/actualutils.aspx?action=gotomsg&tid=894851&msg=20380974

Ещё сотня сообщений... где носители банхаммеров? Давайте скалу обсуждать уже

Хотя что уж, можно и Котлин

инсайдеры сбера есть тут?

в чате про типчики крутой пацан говорил о другом жетбренсовском языке

он похоже тоже ЖВМный, но вот в плане системы типов уделает всякие скалки, хачкили

А может кто пояснить для особо одарённого что я сделал не так? https://pastebin.com/iLM8vx3W

https://twitter.com/groovypodcast/status/851806792984166401

если зарелизится когда-нибудь

а это не шутка?

а это не шутка?

Судя по https://research.jetbrains.org/ru/ — возможно и нет.

он похоже тоже ЖВМный, но вот в плане системы типов уделает всякие скалки, хачкили

сдались тебе эти типы)

сдались тебе эти типы)

а точно... [ушёл в жаваскрипт]

а точно... [ушёл в жаваскрипт]

наш посан

В настоящее время группа работает над созданием формального языка с зависимыми типами, основанного на гомотопической теории типов (homotopytype theory, сокращенно — HoTT). Глобальная цель исследовательской группы заключается в том, чтобы разработать на базе современной теории типов многопользовательскую онлайн-систему верификации доказательств, пригодную для формализации отдельных разделов математики. Идея проекта возникла в 2012 году, когда одна из команд JetBrains занималась совместным онлайн-редактором, основанным на операционных преобразованиях. Соответствующий алгоритм удалось разработать и верифицировать с помощью системы доказательства теорем Coq, а интерес к прикладным аспектам формальной верификации и автоматической проверки доказательств привел к созданию отдельной исследовательской группы. В 2015 году она переключилась на разработку экспериментального языка на основе HoTT. Репозиторий с программным кодом доступен по адресу: https://github.com/valis/vclang

чет звучит совсем фантастически

Да там чат не то, что ваш. Там драмы межнационального характера, не то, что ваши харассменты

И судя по рассказам этого Куклева всё очень даже реалистично

В настоящее время группа работает над созданием формального языка с зависимыми типами, основанного на гомотопической теории типов (homotopytype theory, сокращенно — HoTT). Глобальная цель исследовательской группы заключается в том, чтобы разработать на базе современной теории типов многопользовательскую онлайн-систему верификации доказательств, пригодную для формализации отдельных разделов математики. Идея проекта возникла в 2012 году, когда одна из команд JetBrains занималась совместным онлайн-редактором, основанным на операционных преобразованиях. Соответствующий алгоритм удалось разработать и верифицировать с помощью системы доказательства теорем Coq, а интерес к прикладным аспектам формальной верификации и автоматической проверки доказательств привел к созданию отдельной исследовательской группы. В 2015 году она переключилась на разработку экспериментального языка на основе HoTT. Репозиторий с программным кодом доступен по адресу: https://github.com/valis/vclang

?

чет звучит совсем фантастически

а чего фантастического то?

к тому времени уже дотти2 будет)

> разработать на базе современной теории типов многопользовательскую онлайн-систему верификации доказательств, пригодную для формализации отдельных разделов математики.

вот это

> разработать на базе современной теории типов многопользовательскую онлайн-систему верификации доказательств, пригодную для формализации отдельных разделов математики.

что тебя смущает-то? Этим сотни тысяч людей занимаются по всему миру

что тебя смущает-то? Этим сотни тысяч людей занимаются по всему миру

ну и как успехи?)

ну и как успехи?)

збс, все верят в HoTT

все доказательства до сих пор проверяются и верифицируются вручную перед публикацией

кто изучал математику, понимает, насколько сложные и нелинейные бывают доказательства, их не подгонишь под алгоритм

> разработать на базе современной теории типов многопользовательскую онлайн-систему верификации доказательств, пригодную для формализации отдельных разделов математики.

ты думаешь скала не такая?

или хаскель?

Вот это HoTT - это как-то связано с творчеством Романа Михайлова?

все доказательства до сих пор проверяются и верифицируются вручную перед публикацией

смотря как написаны, доказательства бывают в разных формальных системах, HoTT благодаря конструктивности может быть сформулирована и проверена в языках, поддерживающих соответствующую семантику

кто изучал математику, понимает, насколько сложные и нелинейные бывают доказательства, их не подгонишь под алгоритм

я в школе изучал)

как думаете, не релизную версию scalapb стоит тащить в проект?

сейчас вершина мат. науки - топология, бесконечномерные пространства функциональные, все на языке функана пишется

кто изучал математику, понимает, насколько сложные и нелинейные бывают доказательства, их не подгонишь под алгоритм

вообще тут многие изучали математику, и, стоит, наверное познакомиться категорной логикой и теориями типов, чтобы понять, как это работает, но об этом лучше расскажут чуваки из того чата, ну или хотя бы @clayrat

сейчас вершина мат. науки - топология, бесконечномерные пространства функциональные, все на языке функана пишется

нет там вершины

сейчас вершина мат. науки - топология, бесконечномерные пространства функциональные, все на языке функана пишется

боюсь, что это очень давно - не вершина

боюсь, что это очень давно - не вершина

поправлюсь, эта одни из основных областей исследования

теоркат, типы тоже построены на этом

сейчас вершина мат. науки - топология, бесконечномерные пространства функциональные, все на языке функана пишется

как раз следующий уровень после топологии - теория гомотопий и теория категорий

началось)

как вы это все понимаете

и если объекдинить это всё с высшей алгеброй и наложить на Теорию Типов Мартина-Лёфа, получится HoTT

https://www.youtube.com/watch?v=mqAf5lOJZew

4 года этим занимался, семинары

как вы это все понимаете

я не понимаю, просто вспоминаю отдельные реплики из чатика про типы

Юрий Да, этого чувака я и имел в виду

как раз следующий уровень после топологии - теория гомотопий и теория категорий

это не уровень

это раздел

да не раздел это

Получается, стоит это воспринимать всерьез?

как думаете, не релизную версию scalapb стоит тащить в проект?

что-то страшновато. пока сидим на ванильном протобафе и пишем сериалайзеры руками.

я вот иногда когда смотрю в книгу Кнута у меня голова взрывается

а вы тут вообще жгете

гомологическая алгебра основана на алгебраической топологии

что-то страшновато. пока сидим на ванильном протобафе и пишем сериалайзеры руками.

У меня то ли задач под ProtBuff не было, то ли я не понимаю его сути... :(

просто к слову

что-то страшновато. пока сидим на ванильном протобафе и пишем сериалайзеры руками.

геморойненько

гомологическая алгебра основана на алгебраической топологии

не очень понимаю, почему знак равенства между гомологической алгеброй и теоркатом

4 года этим занимался, семинары

как ты потом на спринг смог уйти?

ERROR: S client not available

был период ломки?

как ты потом на спринг смог уйти?

вот это вообще странно

не очень понимаю, почему знак равенства между гомологической алгеброй и теоркатом

никто не говорит про знак равенства

я лишь про крепкую связь наук

геморойненько

есть такое, все думаем как автоматизировать но пока руки не доходят

я лишь про крепкую связь наук

ну чувак, так можно теоркат и с литературой связать

ну чувак, так можно теоркат и с литературой связать

свяжи

никто не говорит про знак равенства

все эти ветки всё равно основаны на теории множеств, а мы говорим об иных логиках

свяжи

не, я тупой ж

знаешь сам

просто к моим словам выше - топология и функан сейчас заруливают, как области математики

и теория чисел конечно

у меня даже консул не взлетает, о чем тут говорить)

просто к моим словам выше - топология и функан сейчас заруливают, как области математики

ну а Го сейчас заруливает как язык, не повод же игнорирать другие языки

@dmsol после хаусдорфовости и компактности топ. пространств я просто перестал понимать реальность происходящего. Для этого нифиговый матем. бэкграунд нужен.

@dmsol после хаусдорфовости и компактности топ. пространств я просто перестал понимать реальность происходящего. Для этого нифиговый матем. бэкграунд нужен.

сложнее решать задачи на эти темы)

@dmsol таки пришлось решать ?

потому что алгоритма нет, фри плей

ох, чет прям ностальгия

@dmsol я сейчас ударился в теорию категорий, и теперь мне немного неясно, как полностью её понятия связать с понятиями из того же Хаскелла. Есть что-то почитать на эту тему?

потому что алгоритма нет, фри плей

а разве в математике не везде так?

а разве в математике не везде так?

нет конечно

взятие трёхмерного интеграла - алгоритм

решение диффура в ЧП - алгоритм

ну это сейчас это алгоритм

а на момент решения возможно им не было

мой профессор даже называл вот это все бухгалтерией

а типо истинная математика - в доказательствах и исследованиях

@dmsol Нет, конечно, мне хочется сказать, что тип - это категория, а функции - это изоморфизмы между категориями, но хочу определенности)

@dmsol Нет, конечно, мне хочется сказать, что тип - это категория, а функции - это изоморфизмы между категориями, но хочу определенности)

я просто гуглил все подряд на эту тему

статьи с хабра есть неплохие