That’s fair.
I think a better way of putting my point is, can we express the particular behaviors I’m interested in proving, and only have the compiler care about those, rather than checking everything it might be interested in.
That’s fair.
I think a better way of putting my point is, can we express the particular behaviors I’m interested in proving, and only have the compiler care about those, rather than checking everything it might be interested in.