  G{\"o}del's completeness theorem for classical first-order logic is one of
the most basic theorems of logic. Central to any foundational course in logic,
it connects the notion of valid formula to the notion of provable formula.We
survey a few standard formulations and proofs of the completeness theorem
before focusing on the formal description of a slight modification of Henkin's
proof within intuitionistic second-order arithmetic.It is standard in the
context of the completeness of intuitionistic logic with respect to various
semantics such as Kripke or Beth semantics to follow the Curry-Howard
correspondence and to interpret the proofs of completeness as programs which
turn proofs of validity for these semantics into proofs of derivability.We
apply this approach to Henkin's proof to phrase it as a program which
transforms any proof of validity with respect to Tarski semantics into a proof
of derivability.By doing so, we hope to shed an effective light on the relation
between Tarski semantics and syntax: proofs of validity are syntactic objects
with which we can compute.
