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.
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.