>I would like to challenge the assumption here: that programming (in whatever mode) can't be adequately described by mathematics.
Well, the entire lesson of the Halting Problem and Rice's Theorem is that it can't. Indeed, Haskell loves to just cut through the bullshit about math and be inconsistent: bottom inhabits every type, and Type inhabits Type (in Dependent Haskell).
No fixed mathematical system is capable of formally verifying all programs, or even all interesting programs. You always need more bits of axioms than of program if you want to prove theorems about your programs (Chaitin's principle, proved formally by Calude).
What we can say for FP is that Fast and Loose Reasoning is Morally Correct, and that if we use nicely categorical constructions, then when our programs happen to terminate at all, those nice constructions describe their behavior.
Well, the entire lesson of the Halting Problem and Rice's Theorem is that it can't. Indeed, Haskell loves to just cut through the bullshit about math and be inconsistent: bottom inhabits every type, and Type inhabits Type (in Dependent Haskell).
No fixed mathematical system is capable of formally verifying all programs, or even all interesting programs. You always need more bits of axioms than of program if you want to prove theorems about your programs (Chaitin's principle, proved formally by Calude).
What we can say for FP is that Fast and Loose Reasoning is Morally Correct, and that if we use nicely categorical constructions, then when our programs happen to terminate at all, those nice constructions describe their behavior.