NK
О. Вот это соединяет у меня в голове сразу несколько кусков карты
Ну а дальше идея что у нас есть "в одну строчку" переход между эквивалентными представлениями данных - например, между числами Пеано и длинной бинарной арифметикой.
При этом переносятся целые "сложные программы" и доказательства, т.е. (при наличии хорошей системы параметризованных модулей) сокращается количество копипасты и общий объем кода