I like the fact that the first person to implement a full-fledged proof assistant in a computer was a mathematician.

Not a computer scientist.

Not a logician.

Not a philosopher.

His name is de Bruijn.

More precisely, Nicolaas Govert de Bruijn. And he conceived and implemented Automath.

https://en.wikipedia.org/wiki/Nicolaas_Govert_de_Bruijn

Like Brouwer, he is Dutch.

Unlike Brouwer, he was a formalist. I don't think this is recorded anywhere.

But I vividly remember a talk de Bruijn gave at Edinburgh, at an LFCS seminar, when I was there in 1997/1998. At some point Gordon Plotkin asked whether he was a formalist, and he answered "yes" emphatically.

Brouwer, instead, was emphatically non-formalist. Even more non-formalist that my classical mathematician friends.

And, as you know, Brouwer was the main founder of what is known as intuitionistic mathematics, that lead in turn to constructive mathematics. Then the topos theory people picked it up, not for philosophical reasons, but for mathematical reasons. The logic of the internal language of a topos is intuitionistic - this is a theorem, rather than philosophy.

I don't agree with either de Bruijn or Brouwer, but I love their ideas.

I also like that in the 1970's, Bourbaki, known for their excessive formalism, dismissed the idea that mathematics could actually be formalized, when de Bruijn and his collaborators had already done that without their knowledge:

L. S. van Benthem Jutting, as part of this Ph.D. thesis in 1976, translated Edmund Landau's Foundations of Analysis into Automath and checked its correctness.