I don't agree that a-priori truths are limited to axioms—it's a much larger category of "necessary" truths. A theorem which has been proved is an a-priori truth.

Sure, programs are proofs in the context of Curry-Howard. But not necessarily proofs of what you want them to prove.