  Clausal Language (CL) is a declarative programming and verifying system used
in our teaching of computer science. CL is an implementation of, what we call,
$\mathit{PR}{+}I\Sigma_1$ paradigm (primitive recursive functions with
$I\Sigma_1$-arithmetic). This paper introduces an extension of
$I\Sigma_1$-proofs called extraction proofs where one can extract from the
proofs of $\Pi_2$-specifications primitive recursive programs as efficient as
the hand-coded ones. This is achieved by having the programming constructs
correspond exactly to the proof rules with the computational content.
