9 ms·
Formal as in Formal Mathematics -- a specification with a precise definition that can be verified by a model checker to have the desired safety and, if necessar
by agentultra 8y ago
Formal as in Formal Mathematics -- a specification with a precise definition that can be verified by a model checker to have the desired safety and, if necessary, liveness guarantees.
- mehh 8y agoWhich flavour of Formal Mathmatical language would you suggest it should be written in?
- agentultra 8y agoTLA+, Alloy, Isabelle, Coq, or Lean would all be fine choices. I'd prefer TLA+ myself as the language, TLA, is straight-forward maths.
- mehh 8y agoWhat about Z or B?