Меня довольно сильно напрягают те части математики, в которых чтобы сделать какое-то преобразование, нужно проверить 10 разных условий. Даже банальное преобразование
работает далеко не по щелчку пальцев и требует проверять разные условия: нужно чтобы функции
и
были интегрируемы по Риману, т.е. надо проверять их ограниченность, проверять меру множества их точек разрыва на этом отрезке (чтобы удовлетворлся критерий Лебега). И это нам еще повезло: здесь хотя бы не надо контролировать области определения: при "расщеплении" функции
на функции
и
область определения может только расшириться, но не сузиться.
Эффективность математики во многом определяется возможностью делать преобразования без больших мыслительных усилий, "на уровне карандаша". Если преобразование делается не нативно, а требует проверки кучи условий - это плохое преобразование.
Я прихожу к такому выводу, что было бы здорово уменьшить общность, но получить взамен более гладкую технику преобразований. На примере действительного матанализа: если ограничиться элементарными функциями, то, например, не придется заботиться о проверке непрерывности: элементарная функция непрерывна всюду, где она определена. Но это слишком топорное решение. В идеале хочется иметь специальный формализованный язык, в котором можно было бы определять функции
только теми средствами, которые там есть и потом делать с ними преобразования без проверки всякой ерунды. И чтобы компилятор проверял различные условия типа точно ли функция определена там где надо, корректно ли она построена из базовых примитивов языка и тому подобное.
Да, получится так, что средствами такого языка не получится определить какую-нибудь канторову лестницу или даже функцию Дирихле. Да и пофигу, не больно и хотелось. А вот что хочется - так это чтобы в качестве базовой числовой системы было не
. Я сомневаюсь, что подойдет какое-то топорное решение типа вычислимых чисел - это было бы довольно грустно. Хочется, чтобы числовая система была сильно интереснее: можно, например, пожертвовать существованием или алгоритмическим определением нуля (а иметь вместо него "монаду" околонулевых чисел). Вероятно, операции с числами должны быть всюду определенными или по крайней мере с алгоритмической разрешимостью (чтобы компилятор бил по рукам, если пытаешься сделать запрещенную операцию). Можно пожертвовать неограниченностью чисел.
Еще интереснее было бы вносить изменения на уровне логики. Типа как в "дешевых" версиях нестандартного анализа: можно делать всякие непотребства, которые нельзя делать в обычной ситуации, но вот логика - интуиционистская (а значит нельзя пользоваться законом исключенного третьего).