Hacker News Reader

Type systems can encode invariants even on the protocol level. For example you can hand-write or generate (multi party) session types to avoid deadlocks etc.

For Rust there is https://crates.io/crates/session-types from http://munksgaard.me/papers/laumann-munksgaard-larsen.pdf

View on HN

this is an interesting approach that I hope we see more of! but i specifically meant to refer to security components of a protocol: e.g. that whether a party can impersonate another with access to some information that is public or can be disclosed via some attack.

Are you aware of Pi-calculus and ProVerif? ProVerif sounds to address at least some of your requirements. Links: - https://en.wikipedia.org/wiki/%CE%A0-calculus - https://prosecco.gforge.inria.fr/personal/bblanche/proverif/

Reply on news.ycombinator.com