Re: TLA+ theory blog post series + new subreddit

[Steven Stewart-Gallus <stevensele...@xxxxxxxxx>]

This is interesting but IMO doesn't do enough to separate the notion of the program being reasoned about (like PLUSCAL) and the logic for reasoning about it (like TLA+.) Ultimately computer programs are just strings of characters and near enough almost any logic allows you to reason about them. Indeed, there is no reason one couldn't also write a HASKCAL translator that creates TLA+ specs from a functional programming language or a CALLOG translator that creates TLA+ specs from a PROLOG like language. IMO this has been a major mistake of users of systems like Coq. One should not attempt to extract a Haskell program from the Coq type Nat -> Nat. Instead one should extract from a custom type such as Hask Nat Nat.

It might actually be an interesting exercise to extract PLUSCAL programs to Coq code.