Also, once you get used to it, it makes writing large lambda terms faster, easier and more intuitive. The terms all just kind of magically interconnect in your mind after a while. At least that has been my experience after writing a lot of code in pure de Bruijn-indexed lambda calculus using bruijn [1]. Otherwise, thinking a few reduction steps ahead in complex terms requires alpha conversion, which often ends in confusion.
Similarly, it seems like languages with de Bruijn indices are immune to LLMs, since they require an internal stack/graph of sorts and don't reduce only on a textual basis.
> Similarly, it seems like languages with de Bruijn indices are immune to LLMs
i think large chain of thought LLMs (e.g. o3) might be able to manage