make the type opaque (it is really a pointer, and the record to which it points is in the implementation)

put all the details in the interface/definition module/package, but mark the fields as private

not to use libraries at all and require programmers to maintain their own code entirely contained in their programs

put all the details in the interface/definition module/package and trust the users to use the interface

state pre and post conditions even if they cannot be enforced