Is it possible to compute whether two functions are extensional equal?
Yes. If you can verify that they are the same, then so can a computer.

Here's a quick specification for an integer sort in Coq:

Inductive natlist : Type :=
| nil : natlist
| cons : nat → natlist → natlist.

Fixpoint is_sorted (l : natlist ) : bool :=
    match l with
    |  nil =&gt; true
    |  (cons x nil) =&gt; true
    |  (cons x (cons y r)) =&gt; if x &lt;= y then is_sorted (cons y r) else false
    end.

...

Theorem sort_spec : forall l, is_sorted (sort_list l).


A specification can be directly encoded into the declaration of sort using dependent types.

For this particular problem, John Darlington demonstrated in the 70s that 6 families of sorting algorithms can be derived by mechanically transforming the specification of a sort into an implementation; I believe this goes under the name "semantics-based program derivation."

In the software-engineering world, finding extensionally equivalent functions is known as "semantic clone detection."

Dave Clarke also gave a good answer to this question on the CS StackExchange: https://cs.stackexchange.com/questions/2059/how-do-you-check-if-two-algorithms-return-the-same-result-for-any-input

This all falls under the umbrellas of formal methods and programming languages. Denotational semantics are one class of techniques for modeling semantics, but they've fallen out of favor for being difficult to use compared to operational semantics.