 An appropriate mechanization of the language of this intuitionistically non-contradictory mathematics should therefore deliver precisely what the formalist school has set as its goal. (Brouwer 1929A: 164; translation mine)