Duality of 'hard to prove' versus 'hard to compute'

Suppose T is a theorem of mathematics formalised in the language of second-order arithmetic. 
Experience (e.g. Reverse Mathematics) suggests that there is a certain ‘duality’ between the proof theoretic and computability theoretic properties of T, as follows
If T is hard to prove (i.e. requires strong axioms), then T involves objects that are hard to compute, and vice versa. 
Are there (natural) examples of exceptions to this duality?