Introducing tlabyexample.com

[Federico Ponzi]

Hello TLA+ community,

I’ve created a small website, https://tlabyexample.com, which aims to let users learn TLA+ interactively by running TLC in the browser with zero installation required. Please check it out and feel free to contribute on GitHub: https://github.com/FedericoPonzi/tla-by-example.

Background: I managed to run tlatools in the browser using the CheerpJ JVM. I first investigated this while working on a web version of the TLA+ formatter (https://gh.fponzi.me/tlaplus-formatter/), which depends on SANY. I later realized it might be possible to run TLC as well.

I quickly put together a PoC here: https://gh.fponzi.me/tlaplus-web/ (repo: https://github.com/FedericoPonzi/tlaplus-web). Having TLC in the browser might not sound exciting for veteran users, but it enables several useful use cases, such as having a playground that requires no local installation, potentially lowering the barrier to entry for newcomers and serving as an interactive sandbox for playing with specs from the Example repo.

Please share any feedback here or open new issues with ideas, suggestions, or fixes.

Thanks,

Federico

[Felipe Oliveira Carvalho]

Looks great!

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/c0f2fbb8-e95c-4e75-9f66-94926ccdedc0n%40googlegroups.com.

[Markus Kuppe]

This is really great and something many users have been asking for over the years. It's great to see it finally coming together.

Markus

> To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAOC8YXYK5QHtexJLmVJHgR%2BXt%2B-kg5ZwZuJnir6wyuFGj2Ku7A%40mail.gmail.com.

[Andrew Helwer]

Very exciting! Been wanting to make something like the Lean Natural Number Game but for TLA+ for a while, which this would make possible.

Andrew

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/FEA1D44F-F1C9-4CBE-A9FE-CDB902DA7AD0%40lemmster.de.

[Chris Ortiz]

It is really cool when you demo'd it to us during the outreach meeting. It is even accessible on my mobile phone. Like we said in the meeting, the only barrier would be it is not accessible to corporate IT strict internet where we are getting "This site can't provide a secure connection......ERR_SSL_VERSION_OR_CIPHER_MISMATCH". I am not IT expert maybe something you have to configure where you are hosting this. When that get resolved, I plan to direct my coworkers to your website, who in the future will like to start upskilling using TLA+. I also mentioned in the meeting that I am currently working with 23 students on 6 projects related to TLA+ and I can ask them to try your website out to learn more of TLA+, which II am encouraging them to have skill on especially that potentially AI will be their competitor when they graduate and TLA+ skill gives them edge and tools on critical-thinking in terms of systems. 

Fantastic work!!! Many thanks for sharing.

Thanks,

Chris (zitro)