[4ad]

It's very simple, it's because pure, typed functional programming is not arbitrary but rather fundamental. Natural deduction from logic corresponds to various typed lambda calculi, and functional programming is but a practical manifestation of lambda-calculus.

Under Curry-Howard correspondence simply typed lambda calculus is the term calculus for intuitionistic propositional logic. System F (polymorphic lambda calculus) corresponds to impredicative second-order propositional logic. System Fω corresponds to a kind of higher-order logic. Dependent types correspond to intuitionistic predicate logic, etc.

Other correspondences that are based on sequent calculus instead of natural deduction are more exotic, for example classical logic corresponds to μ~μ-calculus, a calculus of continuations which (very) roughly can be understood as continuation-passing style (but in a principled and careful way). Classical linear logic corresponds to a form of session-typed process calculus. Intuitionistic linear logic corresponds to either a process calculus or to a lambda calculus that is using futures (which can be though as mutable shared memory concurrency using write-once cells).

Note however that languages corresponding to sequent calculus, especially ones that come from a dual calculus (classical logic or classical linear logic) contain some sort of commands, choices that you request from a value, which more or less makes them object-oriented languages, albeit without imperative, mutable assignment. In some sense you can escape functional programming by moving to a dual calculus, but you can't escape purity as long as you care about having propositions as types.

From a Curry-Howard point of view no logic corresponds to a general imperative calculus. Imperative programming is simply not fundamental and generally undesirable when doing logic (so when doing type theory). Mutable state with imperative updates can easily be encoded into FP when needed, e.g. via monads, by using linear types, or by having algebraic effects.

That doesn't mean that types are not useful to imperative languages, of course they are. But types in imperative programming are very weak and logically not very interesting however useful they might be for engineering purposes. Also note that type theory does not mean type system. Many languages have type systems, some more ad-hoc than others, but type theories are special, very specific mathematical objects that embody logic (under the Curry-Howard correspondence). All programs written in a type theory terminate, and this is fundamental. Usual programs, which are not concerned with mathematical proofs certainly don't always terminate.

Of course understanding type theory is a very good way of producing (weaker) type systems that are useful in practical programming, including imperative programming (see for example Rust, which does not employ an ad-hoc type system). Occasionally new logic correspondences are discovered which illuminate certain language features of existing languages. For example Rust's borrowing system was thought to be ad hoc, but now we understand that shared borrows correspond to a logic that arises from semi-axiomatic sequent calculus. The cuts that remain after evaluation (normalization), called snips, are precisely shared borrows, while general cut is memory allocation.

The book in the link is a book about Martin-Löf type theory, which means it is a book about a certain kind of lambda calculus by necessity, there is no other choice.

[zozbot234]

> From a Curry-Howard point of view no logic corresponds to a general imperative calculus.

From a CH point of view the logic associated with any Turing-complete language is inconsistent, but this applies to both imperative and functional languages. One could imagine a broadly imperative language without a fully-general "while" construct that could have a useful logical counterpart under CH.

This might be similar to how systems like combinatory logic can in some sense be considered "imperative" languages, since they explicitly act on some kind of logical "state" which works much like state in imperative languages; the only rule of inference being "do A then B then C".

[4ad]

Yes, that's true. And there are various logical systems which hint at mutability (apart from linear logic itself). I already mentioned how we can find shared-memory futures in semi-axiomatic sequent calculus. Those futures are mutable, but write-once. This write-once aspect induces a degenerate monotonicity property which can be generalized to arbitrary monotonicity. Mutable variables can exhibit a form of CH as long as writes to them are monotonic in a certain sense, in particular new writes must not refute old reads. For example logical variables in a logic languages are exactly this. Safe, shareable mutable variables which denote evolving proof state during proof search.