интересно откуда они деньги берут

там только в начале черновик, потом идет Table of contents, а за ним какой-то монстр

Это же стартап. Выиграли финансирование, нашли инвестора

Это не мешает всему документу быть черновиком

инвестиции в язык
ну ок
но они уже давно его пилят

и даже что-то релизили только запустить не оч получалось тогда

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

они миксуют зависимые типы, типы-объединения (которые они получают через row-типы?), какой-то очень странный сабтайпинг (вместо того, чтобы припилить bounded quantification), неявные эффекты (у них там IO можно делать в функции, которая возвращает Int), еще я где-то видел, что у них есть какая-то ленивость (ведь ленивость и неявные эффекты — это то, что так хорошо сочетается). При этом у них таки есть вывод эффектов, но если указываешь явную сигнатуру, то выведенные эффекты тупо выкидываются

не в то окно?

в то. Показываю то, от чего у меня кровопотеря

(могу в другой чатик это все перенести, если тут неуместно)

(но это касается вакансии вверху, так что наверное уместно?)

либо у них nat изоморфен int (но тогда бессмысленно говорить о сабтайпинге), либо они не знают, что правило сабтайпинга для функций выглядит как T1 <: S1, S2 <: T2 => S1 -> S2 <: T1 -> T2

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

тут неуместно

ваши впечатления о работодателе уместны, обсуждать детали не стоит

мои впечатления таковы, что они делают что-то очень странное, а все выше — это аргументация. "Странное" — это необязательно плохо, их ядро выглядит похожим на то, что описано в Pure Subtype Systems:A Type Theory for Extensible Software, но в целом зоопарк типов доверия у меня не вызывает абсолютно

а прочитал я это все потому, что заинтересовался вакансией. Но мне не кажется, что у них science-first подход к дизайну систем типов, так что посылать резюме не стану. Может кому полезны будут мои комментарии