Modeling Redux with TLA+

Re:Modeling Redux with TLA+ by nazri1 on Tuesday March 13, 2018 @04:19AM (#16574504)

Any takers for doing this in lisp? ;)

[ Parent | on HN ]

Re:Modeling Redux with TLA+ by abhirag on Tuesday March 13, 2018 @07:55AM (#16575378)

Not formal verification, but you can specify and validate application state of SPAs written in clojurescript using clojure.spec(https://clojure.org/about/spec).

Example -- (https://github.com/Day8/re-frame/blob/master/examples/todomv...)

[ Parent | on HN ]

Re:Modeling Redux with TLA+ by hwayne on Tuesday March 13, 2018 @11:04AM (#16576655)

You might wanna check out ACL2, which is a theorem prover rooted in common lisp: http://www.cs.utexas.edu/users/moore/acl2/

[ Parent | on HN ]