​Доклад: Программирование на уровне типов на TypeScript — выжимаем из компилятора все соки

В докладе будут рассмотрены нюансы системы типов TypeScript, позволяющие осуществить первые шаги в области формальной верификации программ. Первая часть доклада посвящена методам, которые позволяют инструктировать компилятор выполнять дополнительные проверки на корректность кода, а также обеспечивать соблюдение определённых инвариантов.

Во второй части обсуждают способы описания базовой арифметики с использованием типов, например, как добиться того, чтобы компилятор мог вычислить факториал числа. Завершающая часть доклада касается изоморфизма Карри-Ховарда и демонстрации того, каким образом можно выразить некоторые простейшие силлогизмы математической логики:

https://youtu.be/yBt3t8vzdvs?si=nllTKOK-mA0XZQWt

#доклад #typescript #ru