[mathetic]

The language is just assignment to simple variables (like `=` in C), sequencing (like `;` in C), if-then-else statements, and while loops.

The simple version uses algebraic data types (present in Rust, Haskell, OCaml to name a few) to describe the abstract syntax tree of the language.

The inference rules [0] (the bits that have lots of dashes in them) are standard notation for describing logic and type systems.

The rest of the post uses more advanced types, particularly generalised algebraic data types [1] which allow you to have interesting types that reveal information to the typechecker when you pattern match on them.

If you really want to get into type systems and programming language theory, Types and Programming Languages [2] is a classic.

If you just want to understand the privacy ideas, I describe what the rules are supposed to do in detail, so you can gloss over the actual syntax. The only thing that part adds is that I can make Haskell's typechecker prevent construction of privacy violating programs.

If anything is still unclear, feel free to reach out. I'm happy to explain and elaborate.

[0] https://en.wikipedia.org/wiki/Rule_of_inference

[1] https://en.wikipedia.org/wiki/Generalized_algebraic_data_typ...

[2] https://www.cis.upenn.edu/~bcpierce/tapl/

[CTmystery]

Very helpful, thank you!