Formal design is the practice of designing systems so all logic can be analyzed and tested against. It's in order to define programs before they're run. Writing specs basically. The TLA+ language is commonly used for this. While this approach is relatively slow, it can definitely solidify a formal spec; generally should be used to verify if algorithms work the way they should in production.
While TSA+ is based on discrete math;
PlusCal reads more like a C-style
pramming language which can directly be translated to TLA+. This should help
programmers get around better, and works as a direct replacement for
- Studying the comonad, contravariant and free packages (well, blog posts)