> конструктивная математика не разрешает доказательств от противного, не так ли?

это вроде верно, конструктивизм в себя, кажется, включает интуиционизм; но есть теорема о том, что в интуиционистской математике получаются по факту те же утверждения, только люто-бешено обвешанные отрицаниями (https://en.wikipedia.org/wiki/Intuitionistic_logic#Relation_to_classical_logic : a first-order formula is provable in classical logic if and only if its Gödel–Gentzen translation is provable intuitionistically). конкретно конструктивно доказывается следующий факт: для любого отображения f из множества X в множество его подмножеств существует подмножество, которое не лежит в образе; это построение и есть "диагональный процесс Кантора", он вполне конструктивен: берем множество всех элементов x таких, что x не принадлежит f(x).

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

> проблема останова

это все не требует особой борьбы; и приближенные алгоритмы - тема известная (хотя они к проблеме останова и очень опосредованно относятся), и есть неаппроксимируемые задачи, и есть интересное эвристическое соображение, что даже если задача NP-полная и неаппроксимируемая, почти любое её начальное условие допускает полиномиальное решение; и есть примитивно рекурсивные функции, которые "заранее известно" за какое время окончат работу и уж точно не виснут; и это все полезно знать. Но знание того, что про произвольную программу на ассемблере нельзя выяснить, повиснет она, или нет, тоже крайне полезно (в частности, для того, чтобы понимать, что вот такие обходные пути надо выбирать, это не блажь, а необходимость).

> какие проблемы возникают в анализе при требовании полной конструктивности

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

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