It sounds like what you're talking about is indirection, not abstraction.
If you have to verify that "it does X" by following source files and tracing execution then you're talking about indirection.
An abstraction has mathematically sound laws that can be proven and introduce precise, new semantic layers to a program. By definition one doesn't have to think about the layers underneath the abstraction and can instead think entirely in the abstraction.
The difficulty with abstractions is that few practising programmers know how to think even informally about abstractions. The mistake of substituting abstraction for indirection leads to the misguided notion that virtual methods and classes are "abstractions." However if you try to formalize these abstractions with relations and properties I think you will find most of these proofs difficult, if not downright impossible write. That's a good sign you don't have an abstraction.
Right. All that work on type systems is purely indirection. I want to run my code and the compiler keeps telling me I can't access this place in memory because some other part of my code is borrowing it. Or, what do you mean the commutative property of this type class doesn't hold for my type? Purely directing me away from programming, for sure.
Not always. In C++ and Rust, in many cases the abstraction penalty is completely eliminated by inlining or by making an efficient concrete specialization. If this can be achieved the abstraction penalty is paid only in compile time.
That is just the compiler optimizing out the runtime indirection. The effect on you as a programmer is unchanged: you have to look through the same number of source files either way.
If you have to verify that "it does X" by following source files and tracing execution then you're talking about indirection.
An abstraction has mathematically sound laws that can be proven and introduce precise, new semantic layers to a program. By definition one doesn't have to think about the layers underneath the abstraction and can instead think entirely in the abstraction.
The difficulty with abstractions is that few practising programmers know how to think even informally about abstractions. The mistake of substituting abstraction for indirection leads to the misguided notion that virtual methods and classes are "abstractions." However if you try to formalize these abstractions with relations and properties I think you will find most of these proofs difficult, if not downright impossible write. That's a good sign you don't have an abstraction.