you can call me Rachel можно на ты, если комфортно. я имел в виду, что изготавливать все объекты можно и из чего-то другого, а вот сделать что-то со стрелочками и кванторами (и таким образом "пересесть с иглы формульного одобрения") я не очень понимаю, как: все равно остаются аксиомы и правила вывода. Они, конечно, могут иметь вид диаграмм и правил их преобразования, но по сути это те же формулы ведь (хотя, возможно, и более адекватные), e \circ f = g \circ h. Любую, наоборот, формулу можно записать как коммутативную диаграмму, но она довольно быстро станет impenetrable.

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

Почему-то ещё подумал (это к делу не относится, относится, однако, к логике) - в этой науке и самой по себе (в её существующей форме) есть весьма красивые вещи, не торчащие непосредственно наружу; помимо форсинга (который как раз прикладной), например, замечательные шкалы Крипке в интуиционизме и игры Эренфойхта. А вот как раз "доказательство теоремы о нулях через элиминацию кванторов" или теорема Тарского-Зайденберга выглядят, как помесь ежа с ужом; теория Хрущовского же слишком сложная для меня материя пока что, увы.