[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: TLA+ theory blog post series + new subreddit

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.