alt Hacker NewsSimilar to how lambda calculus "just is" (and it's very elegant and useful for math proofs), but nobody writes non-trivial programs in it...
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...