Смысл MLTT (теория типов мартина лёфа, зависимые типы это её кусочек) в том, что это красивый язык для описания таких неполных по тьюрингу алгоритмов. Мы можем на этом эзотерическом языке программирования написать программу, правильно расставив типы. Компилятор проверит справились ли мы с этим, и если да, то автоматически получается, что мы написали машину тьюринга, которая на определённом классе входов останавливается всегда, не может зациклится. При этом мы можем расширять MLTT вполне определённым образом. Для любого нетьюринг-полного в определённом смысле завершённого класса алгоритмов существует естественное расширение MLTT

Нужно просто добавить хитрый тип, содержащий другие типы. Чем более широкий класс алгоритмов -- тем более извращённый этот тип типов (называемый универсумом). Насколько мне известно самым крутым универсумом, известным нам, сейчас является Π3-reflecting universum. При этом нету ЯП, в котором этот универсум реально был имплементирован.

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

нужен баланс между математикой и программированием

так есть задачи сложнее крадов (точнее, где важна эта гарантия), для них и юзают

ну в расте не сделали, и где он?

решают сложные задачи, но опять на чем же? на простых надежных популярных языках

си, питон

вот в расте сделали борроу чекинг, и где он, а где жс. Люди крады на рубях пишут

сорян, на го

я на питоне)

надежность и простота там, конечно, лучше некуда

да, потому что программисты хотят попроще и понадежней

решают сложные задачи, но опять на чем же? на простых надежных популярных языках

Я пишу на питоне и пхп вообще

Это когда пишу код, 90% времени я херачу пайпы на баше и авк

вот в расте сделали борроу чекинг, и где он, а где жс. Люди крады на рубях пишут

В фронте выбора нет

Там только жс и есть

а на бэке есть, а даже там нода сейчас в топах

Не видел

Ты хотел сказать «Джава»?

В фронте выбора нет

В @haskellru люди на ghcjs хуярят и ничо

так и джава в топе, но это не отменяет ноды же

С ноды вроде на го бегут

так и джава в топе, но это не отменяет ноды же

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

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

(на го)

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

Корочн

Чё вы тут развели

А ну го общаться про раст

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

Понятно о чём ты. Тип странно ныться про "завтипы не нужны" в чате языка, где захерачили регионы

Но я думаю тут просто страх "превратиться в хаскель"

Да ладно, я не спорю что у завтипов есть своя ниша

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

А если внедрять, то это будет говно а не код, не?

нет смысла внедрять это во все языки, вместо этого пишут новые, пока имхо не очень удачно, только про coq я ничего плохого не слышал пока-что, но скорее всего тупо потому, что я новичок в тот же жс не могут никак статическую типизацию внедрить, флоу не так крут, как хотелось бы

Вот и я про это

А чё там кстати с формальным доказательством в раст

Я слышал были какие-то проекты

О чем они?

А чё там кстати с формальным доказательством в раст

Заглохло

А если внедрять, то это будет говно а не код, не?

Если так рассуждать, то код на js должен быть верхом красивости. Нет, проблема не в коде вовсе, а в том, что нужно будет кадры готовить

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

Это типа константные женерики?

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

Там рфц был

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

Там рфц был

Три рфц

А потом приняли четвертый без фразы pi типы

Блядь

я сделал

это

ох тыж ебушки воробушки

никаких ffi впредь

нахуй это дело

это лапша и сатанизм

это лапша и сатанизм

дыа

https://github.com/friktor/deezer-rust/blob/master/src/main.rs

Не знаю как но с токеном свежим если с горем пополам пару раз работало

Обработка ошибок в го стиле на расте это конечно секси

топчик

топчик

(монадного сахарку бы)

бля

час ночи уже

ебать

Расскажите Шрамко про and_then

(монадного сахарку бы)

а, ну похоже в расте это даже не нужно

Ага

Ещё есть ?

Оператор для ркзалтов

Ну это ж нужно пробрасывать ошибки

Мы так не умеем

расскажите про ENV, чтобы access_token в коде не торчал

Лол

Пошлите спамить в дизер от шрамко

Чтоб его забанили

Ещё есть ?

Это более монадно, кстати

Пошлите спамить в дизер от шрамко

подло же

подло же

сам виноват

Вово