This has been formalized in various ways, sometimes by writing down axioms that follow from Brouwer’s philosophical description, other times by constructing models such as sheaf toposes.

Discussion of models for choice sequences in various sheaf toposes (usually involving Baire space or Cantor space) include:

Gerrit Van Der Hoeven? and Ieke Moerdijk, Sheaf models for choice sequences, Annals of Pure and Applied Logic, Volume 27, Issue 1, August 1984, Pages 63-107, DOI

Michael Fourman, Notions of Choice Sequence, Studies in Logic and the Foundations of Mathematics, Volume 110, 1982, Pages 91-105, DOI