@johncarlosbaez by "formalize" do you mean, "rewrite in a computer-checked proof system"?
The definition of a function as a set of ordered pairs was/is a formalisation, but not computer-checked; it just allows us to state in simpler terms the properties a function needs to have.