[Gehinnn]

A good abstraction shouldn't make its usage shorter, it should make the proof that the usage is correct shorter.

This usually means the total amount of assumptions needed to prove everything correct is decreased. (when the code is not actually formally verified, think of "proof length" as mental capacity needed to check that some unit of code behaves as intended)