Безопасность = продвижение + сохранение

Это не слоган геймера, хотя и там такой подход работает. В данном случае речь идет об основном свойстве системы типов. Смысл безопасности в контексте типов означает, что правильно типизированные термы "никогда не ломаются" это значит что термы не оказываются в состоянии когда терм не является конечным состоянием, но при этом не можем продвигаться дальше.

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

В этом подходе мне нравится то, что мы как бы едим "слона по кусочкам", мы делаем два правильных шага и точно знаем, что пока мы их делаем, мы в "безопасности". Таким же образом можно декомпозировать сложные системы на более простые составляющие применяя правило "продвижение + сохранение".

#мысли #программирование