Are the proofs the core of the mathematical aspects of the OpenDP project?

[pdurbin]

Are the proofs the core of the mathematical aspects of the OpenDP project? Are there other facets of the project that are math heavy? Asking for a friend.

[Shoeboxam]

Yes! But in more detail:
Every Transformation or Measurement has an associated proof. And when I say every Transformation and Measurement, I'm not exaggerating: this even includes transformations and measurements (components) built from combinators like the chainers, compositors and amplifiers-- in these cases, the proof is automatically derived from the proof of the constituent components and the proof for the combinator.

We are a relatively young project, though, and realistically there hasn't been enough resources to write proofs for most of the library components. Nevertheless, the framework is designed to be supported by a core of encapsulated proofs that can be composed together. Until these proofs are written and vetted, their respective components remain in "contrib", and require explicit acknowledgement/opt-in from library users. It is important we write these proofs because we don't want to teach users that it's ok to just opt into contrib for everything.

Another thing to keep in mind is that, of course, the "heaviness" of a proof depends on the component you choose to write a proof for, and the level of detail you put into your proof. There is a temporary repository here with some example proofs: https://github.com/opendp/whitepapers/pulls. If you would like to write proofs, we don't expect that you match the level of formalism in those proofs, but your proof should be written such that the algorithm is representable and valid on finite computers, and you should be open to iterations based on feedback from the vetting process. We also don't consider the current Rust code to be the "gold standard" and will adapt it in response to issues raised in the formalization process. However, the current Rust code may be a useful resource to lean on when writing a proof.

[Shoeboxam]

One more thing, the code itself can be math heavy, depending the component and who you talk to. Just in the open PRs on this repo, there's a snapping mechanism that does a significant amount of bit twiddling of floating point numbers, an autodifferentiation tool in PyTorch, an analytic gaussian mechanism, and there's a discrete gaussian mechanism hidden on a branch. There's also the PR on F-differential privacy, which I haven't had the time to tear down yet. We also have a need for a utility testing framework. So yes, there are many facets of the project that are math heavy.