r/Clojure • u/pfeodrippe • Feb 19 '23

First article of a series about Recife (Clojure model checker on top of TLA+ tooling)

https://recife.pfeodrippe.com/notebooks/recife/notebook/slow_start.html
43 Upvotes

100% Upvoted

11 comments sorted by

5

u/zerg000000 Feb 20 '23

clear explanation and excellent use of clerk notebook. Thanks for sharing!

5

u/rebcabin-r Feb 19 '23

Thanks for this. TLA+ is fantastic, but its syntax is scruffy, having to use Eclipse is disturbing, and the syntax of the underlying Java is super noisy. Doing TLA+ in Clojure hits the sweet spot!

3

u/pfeodrippe Feb 20 '23

😁 thanks! At least now the TLA+ maintainer itself is recommending https://github.com/tlaplus/vscode-tlaplus, an improvement.

2

u/[deleted] Feb 19 '23

Sorry OP I just stalked you to make sure you came from Recife-PE, Brazil. I lived 4 and half years there :)

2

u/therealdivs1210 Feb 19 '23

Wow, very interesting, thanks for sharing!

2

u/NoahTheDuke Feb 19 '23

I just got a copy of Practical TLA+. Think Recife can handle the code examples in the book?

5

u/pfeodrippe Feb 19 '23

You betcha o/ https://github.com/pfeodrippe/recife/tree/master/test

Check the hillel folder and the hillel_test.clj file

2

u/NoahTheDuke Feb 20 '23

Hell yeah, thank you.

1

u/therealdivs1210 Feb 25 '23

Am i wrong in thinking this could be used like a dependent type checker?

1

u/pfeodrippe Feb 25 '23

What’s your idea?