Безопасность = продвижение + сохранение Это не слоган геймера, хотя и там такой подход работает. В данном случае речь идет об основном свойстве системы типов. Смысл безопасности в контексте типов означает, что правильно типизированные термы "никогда не ломаются" это значит что термы не оказываются в состоянии когда терм не является конечным состоянием, но при этом не можем продвигаться дальше. Чтобы исключить тупик нам нужно гарантировать две вещи: - продвижение - правильно типизированный терм не может быть тупиковым, поэтому мы можем выполнить следующее правило вычисления - сохранение - если терм проделывает шаг вычисления, то полученный терм так же правильно типизирован, а это значит, что можем делать продвижение В этом подходе мне нравится то, что мы как бы едим "слона по кусочкам", мы делаем два правильных шага и точно знаем, что пока мы их делаем, мы в "безопасности". Таким же образом можно декомпозировать сложные системы на более простые составляющие применяя правило "продвижение + сохранение". #мысли #программирование