Is there a proof assistant in which a module (for example, one code file) can expose a constant while not exposing its definition?
It might be useful for a module to define, for example, a natural number addition function, without revealing whether the function works by recursion on its first or second argument.
Proof Assistants
Proof Assistants