I agree with you, but so far I have never been able to get into the logic of de Bruijn's clues. As for example John Tromp knows how to do. (https://tromp.github.io/) But I don't despair of getting there one day...
It's literally just notation:
- It doesn't matter how you name variables. (if you want to sound cool: "lambda terms are invariant under alpha-conversion")
- Each new variable introduces a scope.
- Therefore, how scopes are nested defines the entire expression.
- Instead of the usual way, we represent scopes with numbers, with the index representing "how nested the scope is". Imagine it's python, and you're pressing tab that many times.
Look at how ugly decorators are in python when in lisp you get them for free and they don't even need a name.
Python is optimized towards simple pseudo-code like imperative OOP. That's easier for most programmers.
You might not have noticed the userid of the person you're replying to ;)