-
Notifications
You must be signed in to change notification settings - Fork 50
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
"publicly opaque" concept would be useful when working with laws #1504
Comments
So in summary, it would be interesting to have a notion of "private" vs "public" implementations: so
|
can use the |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
when working with laws in trait, for example:
I would like to be able to make the
serialise
anddeserialise
functionsopaque
from the outside of a class implementing this trait, so that the proof does rely only on the laws. However, I'd like the functions to not beopaque
inside the class definition itself.Here for example, a class implementing the trait
Serialiser
should be able to see its own implementation ofserialise
anddeserialise
to prove that the laws hold. However, other classes having access to an instance of such class shouldn't be able to access the implementation details, but only the laws.Ex:
The text was updated successfully, but these errors were encountered: