Нужна ли программисту математика?
 
Ну, попробуйте написать код на 20-30 строк, не зная арифметику :)
В частности, арифметику булевого типа.
 
Для миддлов сеньоров будет странно, если они например не знают арифметику функций или множеств. В таком случае это будут просто технически хорошо прокаченные джуны, и не более :)
 
Кто говорит, что "программисту математика не нужна", сам не владеет базовой математической логикой (что естественное следствие такой посылки :), потому что очевидно, что есть разница между
"все программисты могут извлечь выгоду из изучения математики" и
"все программисты должны изучать математику".
 
Совершенно точно, каждому сеньору можно подобрать по крайней мере одну область математики, изучение которой принесёт ему пользу в контексте его прямой работы (теория типов, например).
 
Другое дело, что если собрать 100 случайных программистов и заставить их изучать матан, вряд ли он будет полезен более чем 2-3%. Однако если их обучать регуляркам (алгебра Клини), то это будет полезно, ну, минимум 50%. И т.д.
 
=
 
Я в этом плане принудительно экспериментирую над ментатами :) например через теорию типов до HoTT, и пока отзывы были очень положительные, хотя в целом результат выражается в первую очередь в мощной думательной тайп-машинке, что по критерию объективной пользы измеряется довольно слабо.
 
Поэтому думаю, на чём сделать акцент дальше именно в плане чистой математики (так-то прикладные формальные темки разбираем на Функциональных архитектурах), но с потенциальной привязкой к AI.
 
Примерных  направлений тут два: во-первых, теория категорий - суперпрокачка в свёртке и декомпозиции сложнейших понятий, хотя возможно чрезмерно абстрактная (а может быть это как раз и хорошо).
 
и во-вторых, теория моделей (FOL, логика предикатов). Описываем свой домен формально - как класс моделей (семантика), после чего пытаемся определить, а какая теория у этого класса (синтаксис), какие аксиомы, какая алгебра (например, Линденбаума).
 
Проблема что такая теория будет скорее всего неразрешимой, если класс содержит хотя бы арифметику :) Ну и так-то, вычисление теории по классу задачка - о-го-го (множество всех логических следствий из аксиом)...
 
Хотя с другой стороны любой программист этим по сути и занимается, пытаясь фактически реализовать теорию для своего домена говнокодом на коленке :) просто не имея ни малейшего представления о том, что он по сути занимается сложной математической темкой; в этом собственно и прячется сложность, с которой разработчик ведёт постоянную борьбу, и чаще всего безуспешно.
 
...И хорошо бы такую теорию как-то выразить формально, SAT-солвер не потянет (только пропозициональные переменные), SMT? Ну возможно, через DPLL(T)...
 
А если в теорем-пруверах вроде Lean? Тут мы сразу работаем внутри исчисления, а тактики прувера будут исследовать структуру нашей кастомной алгебры, выводя разные следствия. Но это слишком трудоёмко.
 
...В итоге мы попадаем в ту самую область, где именно по этому золотому стандарту и верифицируют чипы, и софт для критических инфраструктур :)
 
Да, но ведь любой математик скажет, что FOL захлебнётся в кванторах уже на сотне сущностей, а как тогда формально верифицируют чипы на тысячи регистров, софт с тысячами классов?
 
(продолжение будет для ментатов на Функциональных архитектурах, остальные могут проконсультироваться у ЖПТ :)