Similar to how lambda calculus "just is" (and it's very elegant and useful for math proofs), but nobody writes non-trivial programs in it...

Make that almost nobody.

I wrote a non-trivial lambda program [1] which enumerates proofs in the Calculus of Constructions to demonstrate [2] that BBλ(1850) > Loader's Number.

[1] https://github.com/tromp/AIT/blob/master/fast_growing_and_co...

[2] https://codegolf.stackexchange.com/questions/176966/golf-a-n...