3 ms·
I've been programming for a while, but can't make heads or tails of the 'simple imperative language'. What is the prereq for understanding this?
by CTmystery 5y ago
I've been programming for a while, but can't make heads or tails of the 'simple imperative language'. What is the prereq for understanding this?
- ok123456 5y agoKnowing Haskell and GADTs.
- mathetic 5y agoThe 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 https://en.wikipedia.org/wiki/Rule_of_inference [1] https://en.wikipedia.org/wiki/Generalized_algebraic_data_type https://en.wikipedia.org/wiki/Generalized_algebraic_data_typ... [2] https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/
- CTmystery 5y agoVery helpful, thank you!