>It is somewhat surprising that unification is cleaner and easier to implement in an loopy imperative mutational style than in a recursive functional pure style. Typically theorem proving / mathematical algorithms are much cleaner in the second style in my subjective opinion.
This is the Curry–Howard correspondence.
While it seems everyone wants to force individuals into one of the formal vs constructivist, it is best to have both in your toolbox.
Contex and personal preference and ability apply here, but in general it is easier for us mortals to use the constructivist approach when programming.
This is because, by simply choosing to not admit PEM a priori, programs become far more like constructive proofs.
If you look at the similarities between how Church approached the Entscheidungsproblem, the equivalence of TM and lambda calculus, the implications of Post's theorm and an assumption of PEM, it will be clear that the formalist approach demands much more of the programmer.
Functional programming grew out of those proofs-as-programs concepts, so if you prefer functional styles, the proofs are the program you write.
Obviously the above has an absurd amount of oversimplification, but I am curious what would have been different if one had started with more intuitional forms of Unification.
For me, I would have probably just moved to the formalist model to be honest like the author.
I just wanted to point out there is a real reason many people find writing algorithms in a functional/constructivist path.
There's absolutely a constructivist form of unification, the description of a particular unification algorithm is typically a rewrite system (OP has one here: https://www.philipzucker.com/assets/traat/unify_rules.png) which qualifies as constructive imho (it builds an explicit solution, ie a substitution). But the imperative implementation of such a rewrite system can be readable too (especially if you still have pattern matching as in, say, Rust or OCaml).
I don't think there's any link to be had with the Curry Howard correspondence here. No types, no lambda calculus, nothing of the sort.
When I was saying 'easier' if we chose to do logic inside a theory using the Curry-Howard correspondence then we find out that it is intuitionistic, and as you mentioned 'proofs' that means it may be important to you vs. someone who is say using lambda calculus as just a programing language.
The Curry-Howard correspondence results in an isomorphism 'Programs'(Haskel Functions) and intuitional proof systems, if you assume they are traditional proofs internally you will have a bad time.
What is important is what we lose in respect to what we often assume due to the typical conventions.
Note that this has been a popular resource to introduce the concepts for a while, and I was encouraging you to mostly learn the tradoffs of call/cc to help on that path and avoid globals, not that it is the only or even good solution.
> This course is an introduction to the research trying to connect the proof theory of classical logic and computer science. We omit important and standard
topics, among them the connection between the computational interpretation
of classical logic and the programming operator callcc.
Grounding and negation as failure are also popular, especially with ML which under the VC dimensionality interpretation of learnability is still a choice function due to the set shattering.
This is the Curry–Howard correspondence.
While it seems everyone wants to force individuals into one of the formal vs constructivist, it is best to have both in your toolbox.
Contex and personal preference and ability apply here, but in general it is easier for us mortals to use the constructivist approach when programming.
This is because, by simply choosing to not admit PEM a priori, programs become far more like constructive proofs.
If you look at the similarities between how Church approached the Entscheidungsproblem, the equivalence of TM and lambda calculus, the implications of Post's theorm and an assumption of PEM, it will be clear that the formalist approach demands much more of the programmer.
Functional programming grew out of those proofs-as-programs concepts, so if you prefer functional styles, the proofs are the program you write.
Obviously the above has an absurd amount of oversimplification, but I am curious what would have been different if one had started with more intuitional forms of Unification.
For me, I would have probably just moved to the formalist model to be honest like the author.
I just wanted to point out there is a real reason many people find writing algorithms in a functional/constructivist path.