Terence Tao's proof of Hilbert's Nullstellensatz

Stream: maths

[Kenny Lau]

In this post by Terence Tao, he proved Hilbert's Nullstellensatz in a more elementary and computational manner. My question is: how constructive is this proof?

[Mario Carneiro]

I believe it is constructive, but note:

in an explicitly computable fashion (using only the operations of addition, subtraction, multiplication, division, and branching on whether a given field element is zero or non-zero)

Of course "branching on whether a given field element is zero or non-zero" means he needs decidable equality for the base field, so the most obvious application, for the base field C, doesn't work without a bit of nonconstructive magic. However there are decidable algebraically closed fields; the algebraic numbers have decidable equality and are algebraically closed so would probably work with the proof.