3 ms·
The perception of FP as being somehow more "math-y" is nothing but a bias. There is no intrinsic magical property of "mathiness", it's just that the operational
by vezzy-fnord 11y ago
The perception of FP as being somehow more "math-y" is nothing but a bias. There is no intrinsic magical property of "mathiness", it's just that the operational semantics of functional languages are much more well-defined. Logic programming is itself firmly based in axiomatic semantics and has a similar a priori system of reasoning to it, though distinct from FP. Imperative languages can be modeled well on Hoare logic, too, and Dijkstra did plenty of research on it, known as predicate transformer semantics. It is comparatively understudied, though.
- agumonkey 11y agoHow come is it a bias ? FP takes root in recursive functions, and inductive reasoning. The same ideas we learn in math classes. And describing pre / post invariants of imperative statements, turns them into typed functions isn't it ? I'm having a hard time seeing the difference.
- alexlarsson 11y agoAlso, many purely mathematical models of computing like turing machines are definitely not functional.
- Yomammas_Lemma 11y agoWell, nobody is proposing that Turing Machines be the foundation of mathematics, whereas the sort of type theory used in FP is being taken pretty seriously as a foundation.
- mafribe 11y agoI agree that FP isn't more mathematical than other forms of programming. the operational semantics of functional languages are much more well-defined. No. The operational semantics of any language that has a compiler or interpreter is as well-defined as possible. What you may mean is that the meta-theory of (pure) FP is better understood than the meta-theory of other paradigms, typically because FP has simpler meta-theoretic properties. Logic programming is itself firmly based in axiomatic semantics This is a non-standard use of the term "axiomatic semantics" which is usually referring to Hoare-logic with pre- and post-conditions. Prolog has (simplifying a bit) a proof-theoretic / proof-search / resolution-unification-based semantics. [Hoare-logics for imperative languages] is comparatively understudied, though. That used to be the case, but the last decade has seen extreme progress in this matter, and Hoare logics for imperative languages are routinely used these days.