Агата Сомова · старший инспектор
«Машина, которая приняла дело, никогда не зависнет». Я годами читала эту фразу как одно обещание. Арбенина пишет на странице «Допуск», что их два: допущенное дело не встанет на полпути и по дороге не поменяет ярлык. Хочу понять, почему двух хватает. И почему одного мало.
Ярлык ставят один раз, на входе. Дело потом идёт десятки шагов, и каждый шаг переписывает терм. Вопрос Сомовой из прошлого урока остаётся: откуда проверке на входе знать, что случится на сотом шаге?
Ответ TAPL помещается в одну строку: безопасность = продвижение + сохранение типа. По-английски progress и preservation, эти слова ты встретишь в любой статье о типах; в курсе дальше говорим по-русски. В этом уроке ты разберёшь каждую половину, увидишь, как они складываются в обещание Кодекса, и сам докажешь первую половину для судьи.
урок из курса
Урок из курса «Логика и типы». Курс покупается один раз и остаётся навсегда: 500 ₽.
Оплата пока не подключена: премиум и курсы открываются промокодом.