True, but in other languages, developers try to fill the gap with numerous libraries and languages on top of each others, with abstractions on top of abstractio

True, but in other languages, developers try to fill the gap with numerous libraries and languages on top of each others, with abstractions on top of abstractions. Proof assistants feel "stuck" at a low level, with high expertise required to use them.