ЭФ>> Этот раздел как называется?
lpd> мат. логика

Ну хорошо, что же математики там наизучали про функцию?
Перечисли, пожалуйста, основные понятия и достигнутые математиками результаты.

«Математики изучают свойства композиции функций, то есть способа (одного единственного!) создания новой функции, объединяя две или более других функций»
— асоциативность
— некоммутативность
— идентичность
— обратимость
(ну и что? Что на практике из этого можно сделать/извлечь для доказательства корректности, а не для оптимизации кода)

«Математики изучают (зачем это надо программистам-не-криптографам?) условия, при которых функция имеет обратную функцию, а так же способы нахождения обратной функции»

Допустим, что всё это выливается в компиляторе в систему статической проверки типов при компиляции.
Но это же не обеспечивает корректности программ! Да, наверное становится лучше, чем было,
но гарантирует мало что. Как ошибки в программах были, так и остаются.

ЭФ>> Этот раздел как называется?
lpd> мат. логика

Ну хорошо, что же математики там наизучали про функцию?
Перечисли, пожалуйста, основные понятия и достигнутые математиками результаты.

«Математики изучают свойства композиции функций, то есть способа (одного единственного!) создания новой функции, объединяя две или более других функций»
— асоциативность
— некоммутативность
— идентичность
— обратимость
(ну и что? Что на практике из этого можно сделать/извлечь для доказательства корректности, а не для оптимизации кода)

«Математики изучают (зачем это надо программистам-не-криптографам?) условия, при которых функция имеет обратную функцию, а так же способы нахождения обратной функции»

Допустим, что всё это выливается в компиляторе в систему статической проверки типов при компиляции.
Но это же не обеспечивает гарантирует корректности программ! Да, наверное становится лучше, чем было,
но гарантирует мало что. Как ошибки в программах были, так и остаются.