4 ms·
And yet Agda, which is a proof language, was included (in the ML family). Looking at some TLA+ examples, I’d say, squinting a bit… somewhere around Prolog ? I’
by navaati 3y ago
And yet Agda, which is a proof language, was included (in the ML family).
Looking at some TLA+ examples, I’d say, squinting a bit… somewhere around Prolog ? I’d love to hear someone chip in !
- colanderman 3y agoYes, having used both TLA+ and Prolog extensively, they share many similarities (both having roots in first-order logic). In practice -- TLA+ code is often a bit more "imperative" owing to the fact that unbounded existential quantification isn't implemented in the TLC interpreter (whereas in Prolog, it is a core aspect of any interpreter). And of course, TLA+ has a suite of temporal operators used exclusively for declaring contracts in service of its role for verifying specifications. Which (as @hwayne points out elsewhere) stem from mathematics -- Linear Temporal Logic specifically -- and not programming.
- Warwolt 3y agoEh, even though you prove things about your specs (possibly) there's still a difference between proof assistances and spec languages