How does the “proofs as programs” correspondence work for equality? The equality relation $=$ can be represented as a type, just as any other propostion in the Curry-Howard correspondence.
I understand the sense in which the basic logical symbols $\land,\lor,\to, \forall, \exists,\neg$ correspond to type constructions, and the sense in which a proof that has a type is a program (e.g. a proof of $A\to B$ is a program that takes a proof of $A$ and outputs a proof of $B$).
But how is a proof of $a=b$ a program? What is the general idea here? I haven’t seen a clear explanation yet.
 A: As Zhen Lin has mentioned in the comments, the specifics will depend on how you are interpreting $=$ in your type theory. Here I will outline how $=$ is handled in
HoTT for concreteness, but you will see that once we have a fixed type representing equality, everything works how you would expect.
In HoTT, we add the following inference rule to our logic:
$$\frac{\Gamma \vdash A \text{ type} \quad \Gamma \vdash a, b : A}{\Gamma \vdash a =_A b \text{ type}}$$
That is, for every type $A$, and for every two values $a,b : A$, we assert the existence of a type $a =_A b$. Values inhabiting this type are proofs that $a$ and $b$ are equal.
To talk about how values $p : a =_A b$ are programs, we will talk about their introduction/elimination rules. I'm going to play slightly fast and loose with my notation here to try and keep the rules legible. If you want the gory details, see the appendix in the HoTT book linked above.
There is only one introduction rule:
$$ \frac{\Gamma \vdash A \text{ type} \quad \Gamma \vdash a : A}{\Gamma \vdash \text{refl}_a : a =_A a}$$
There is always a proof $\text{refl}_a$ (for reflexivity) asserting that $a=a$.
The elimination rule is rather subtle. It forms the basis of what is called "path induction" in HoTT, and is a common source of confusion when getting started. I won't go into too much detail about these subtleties here, though.
$$ 
\frac{
\Gamma, p:a =_A b \vdash C(p) \text{ type} 
\quad 
\Gamma, a_0 : A \vdash c(a_0) : C(\text{refl}_{a_0})
}{
\Gamma \vdash \text{ind}_{=_A}(c) : C(p)
}
$$
This says that given any type family $C$ depending on $p : a =_A b$, if we can eliminate the only introduction rule, then we can eliminate the entire type. That is, if some $c(a_0) : C(\text{refl}_{a_0})$, then we can get a value $\text{ind}_{=_A}(c) : C(p)$ for any $p : a =_A b$ we like. Moreover, $\text{ind}_{=_A}$ satisfies the computation rule:
$$(\text{ind}_{=_A}(c))(\text{refl}_a) = c(a)$$
If it seems surprising to you that we get all of this expressivity by working only with $\text{refl}_a$, you're in good company. This is just the tip of the "subtlety" iceberg that I was referring to earlier. Intuitively, since $\text{refl}_a$ is the only constructor for an equality type, once we prove something for it, we've proven something for the whole equality type. This is analogous to proving something for every value in $\mathbf{1}$ by proving it for $\ast : \mathbf{1}$. The only difference is in our heads: We like to imagine $\ast$ as being the only element of $\mathbf{1}$, while it's easy for us to imagine multiple possible elements of $a =_A b$, especially since our only constructor is for $a =_A a$, which feels like a weaker condition.
Of course, type theory doesn't care about our hang-ups. There are plenty of models of type theory with equality where $\text{refl}_a$ honestly is the only value of any equality type.
As for actually "computing" things with equality types, the obvious practicality of the rest of the lambda calculus breaks down somewhat. While we are technically programming, I'm not sure if there's any analogue of equality types that, say, a software engineer might care about. This is in stark contrast to other constructions in type theory, which correspond to algebraic datatypes (and which thus have obvious real-world computational applications we can point to). I'm sure somebody has thought of what these types can properly compute, but I'm not familiar with any literature on the subject.

I hope this helps ^_^
A: The general idea behind proof-as-program is the same for all propositions-as-types.
You wrote:

a proof of A→B is a program that takes a proof of A and outputs a proof of B

I would rather write:

a proof of A→B is a program that takes a term of type A and outputs a
term of type B

In the same way, a proof of $a=b$ is a program that takes the terms $a$ and $b$ and outputs a term of type $a=b$. Depending how equality is defined in your type theory, a term of $a=b$ might be different things, but that's another story...
In the idea behind proof-as-program, the program is computing on terms, not on proofs. From propositions-as-types you get proofs-as-terms, but a term with a variable is a program, thus you have terms-as-programs and therefore proofs-as-programs...
