Это что-то новое?

А то ведь есть сберклауд

походу да, уже 2 раза звали разные HR туда работать, говорят “как амазон”

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

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

пользователя, все никак форму логин/пароль продраться не могу

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

Я сегодня не мог к Амазону через SAML подключиться. Видимо Амазон штормит.

При
этом мы не рассчитываем, что читатель владеет зависимыми типами на
продвинутом уровне.


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

Итак, основным отличием Arend от других языков с зависимыми типами является
логическая теория, на которой он основан. В Arend в качестве таковой используется
открытая недавно В. Воеводским гомотопическая теория типов (HoTT). Если точнее,
то Arend основан на разновидности HoTT под названием «теория типов с
интервалом». Напомним, что Coq основан на так называемом исчислении
индуктивных конструкций (Calculus of Inductive Constructions), а Agda и Idris — на
интенсиональной теории типов Мартин-Лёфа. Тот факт, что Arend основан на HoTT,
существенно влияет на его синтаксические конструкции и работу алгоритма
проверки типов (тайпчекера). Эти особенности мы и собираемся обсудить в
настоящей статье.

ебучие инопланетяне

Гомотопическая теория типов (или коротко HoTT) — это разновидность
интенсиональной теории типов, отличающаяся от классической теории типов
Мартин-Лёфа (MLTT, на которой основана Agda) и исчисления индуктивных
конструкций (CIC, на котором основан Coq) тем, что в ней наряду с утверждениями
и множествами присутствуют так называемые типы более высокого
гомотопического уровня.

после этого я потерялся

и понял что зашел не в свой двор

Хорошо быть не программистом, мне такое даже читать не стоит (=