Nonconstructive proofs, such as those involving ultraproducts, often contain a "hidden combinatorial core". Techniques from proof theory can systematically expose this effective content. In joint work with Henry Towsner we have examined nonstandard proofs of theorems like the differential Nullstellensatz, giving an alternative perspective on recent results of Freitag, Gustavson, Leon Sanchez, Ovchinnikov, and others.