Yes. Compare also https://www.khoury.northeastern.edu/home/cmartens/Courses/74... where the abstraction itself mechanically enforces certain guarantees and contracts.