Здравствуйте, gandjustas, Вы писали:

G>Кроме того они фактически прикрутили доказательство теорем к системе типов, которое учитывает control flow в программе. И работает система доказательств в обе стороны — для проверки корректности и для вывода типов.

Это, конечно, очень хорошо. Но нужно иметь в виду, что система типов TypeScript "deliberately unsound", т.е. гарантий того, что типы сойдутся в runtime, нет. Кроме того, она undecidable, что в компиляторе решается некоторыми произвольными ограничениями на сложность выводимых типов.