First, you can mathematically reason about a program written in any language; I do it all the time with TLA+ [1]. It is certainly not the case that FP is more a

First, you can mathematically reason about a program written in any language; I do it all the time with TLA+ [1]. It is certainly not the case that FP is more amenable to mathematical reasoning than imperative code, although the kind of reasoning is different: FP mostly relies on equational reasoning while imperative mostly relies on assertional reasoning. Synchronous programming, for example, relies on temporal reasoning. Second, mathematical reasoning has its limits, especially as we're dealing with intractable problems. It doesn't matter if you can somewhat more easily reason about a simple three-line program in one paradigm than in another if most important programs are six orders of magnitude bigger. Unfortunately, program correctness (aside from some very simple properties) does not compose tractably (i.e. even if reasoning about components A1...An is "easy", reasoning about the composition A1 ∘ ... ∘ An can be more difficult than any computable function of n. So I would not put ease of mathematical reasoning about simple cases as necessarily the main priority, let alone the only one. [1]: https://pron.github.io/tlaplus https://pron.github.io/tlaplus