Is program extraction from constructive proofs a real thing?

Yes, it is. Research groups in Japan, the States, the United Kingdom, Sweden and Germany have been active in this area for many years [14, 18, 23, 30] A constructive proof of (let's use this one again) Picard‘s Theorem PTs really does contain an extractable algorithm for computing the point z with the properties stated in the conclusion of that theorem. Moreover, the proof is itself a proof that the program is correct—that is, meets its specifications. So the constructive result gives us two things for the price of one: an algorithm and a proof of its correctness. That's a real bargain!