Существенное использование аксиомы выбора означает крайнюю степень неконструктивности, да. Особенно там, где оно выходит за рамки каких-нибудь вариантов счетного выбора (ультрафильтры на натуральных числах -- выходят).

Под вывеской computer science, как я понимаю, проходят, в том числе, вполне корректные математические теории и результаты. А пользу и возможности программирования лучше всего иллюстрирует сайт livejournal.com, на котором мы ведем эту беседу.