med-mastodon.com is one of the many independent Mastodon servers you can use to participate in the fediverse.
Medical community on Mastodon

Administered by:

Server stats:

364
active users

#tlaplus

0 posts0 participants0 posts today
Andrew Helwer<p>June TLA⁺ development update: AI contest submission deadline is July 4th, Spectacle gets GraphViz animation support, VS Code extension gets MCP support, and a new research grant for synthesizing inductive invariants!</p><p><a href="https://foundation.tlapl.us/blog/2025-06-dev-update/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">foundation.tlapl.us/blog/2025-</span><span class="invisible">06-dev-update/</span></a></p><p><a href="https://discuss.systems/tags/TlaPlus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TlaPlus</span></a></p>
Andrew Helwer<p>I wrote a blog post version of my talk at the 2025 TLA⁺ Community Event last week. I try to capture the current state of TLA⁺ tooling development: what tools exist, our greatest challenges, and what I want in the near-mid future.</p><p><a href="https://ahelwer.ca/post/2025-05-15-tla-dev-status/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">ahelwer.ca/post/2025-05-15-tla</span><span class="invisible">-dev-status/</span></a></p><p><a href="https://discuss.systems/tags/TLAPlus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TLAPlus</span></a></p>
Andrew Helwer<p>Understandable &amp; predictable performance has its benefits!</p><p><a href="https://discuss.systems/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FormalMethods</span></a> <a href="https://discuss.systems/tags/TLAPlus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TLAPlus</span></a> <a href="https://discuss.systems/tags/ModelChecking" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ModelChecking</span></a></p>
Andrew Helwer<p>My talk from the TLA+ community conference has been posted! It's a not-very-technical talk where I go over what's happening in the TLA+ language tooling development space, what challenges we are facing in TLA+ development &amp; how the TLA+ Foundation has been funding work to overcome them, and what I'd like to see come next for TLA+!</p><p><a href="https://www.youtube.com/watch?v=KrhZebeRn90" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">youtube.com/watch?v=KrhZebeRn9</span><span class="invisible">0</span></a></p><p><a href="https://discuss.systems/tags/TLAPlus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TLAPlus</span></a></p>
Andrew Helwer<p>Making a minimal TLA+ model checker for the “build your own TLA+” tutorial has been technically tricky, a puzzle with a lot of dead ends. If a model checker didn’t already exist I doubt I’d believe it possible. Admiration for Yuan Yu for writing one in the first place, back in the day.</p><p><a href="https://discuss.systems/tags/TLAPlus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TLAPlus</span></a></p>
Andrew Helwer<p>Neat proposal on gathering usage analytics for a FOSS project. No analytics gathered by default, but the program issues a DNS query for “programname-eus”. Corporations (or anyone) who run DNS servers for their internal network can add an entry for programname-eus.corpname.com which directs to a usage capture database. If the entry is present then analytics become opt-out instead of opt-in. Good for corporations who want to fund the project being able to track internal usage.</p><p><a href="https://github.com/tlaplus/tlaplus/issues/1170" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">github.com/tlaplus/tlaplus/iss</span><span class="invisible">ues/1170</span></a></p><p><a href="https://discuss.systems/tags/FOSS" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FOSS</span></a> <a href="https://discuss.systems/tags/TLAPlus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TLAPlus</span></a></p>
Andrew Helwer<p>Today's work: finished the tutorial on parsing &amp; interpreting basic constant TLA⁺ expressions. Not too different from any calculator app tutorial you've seen, but had to get the foundations in. All credit for the teaching technique goes to wonderful textbook Crafting Interpreters by Robert Nystrom.</p><p><a href="https://docs.tlapl.us/creating:expressions" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">docs.tlapl.us/creating:express</span><span class="invisible">ions</span></a></p><p><a href="https://discuss.systems/tags/TLAPlus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TLAPlus</span></a></p>
Andrew Helwer<p>Today I discovered that TLA⁺ parses 1 + 1 - 1 as (1 + (1 - 1)), PEMDAS heads absolutely BTFO</p><p><a href="https://discuss.systems/tags/TLAPlus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TLAPlus</span></a></p>
Andrew Helwer<p>March TLA+ development update: a bad month for tuple-except expressions, another formal methods use paper from AWS after 10 years, a new TLA+ formatter written in Rust, and more!</p><p><a href="https://foundation.tlapl.us/blog/2025-03-dev-update/index.html" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">foundation.tlapl.us/blog/2025-</span><span class="invisible">03-dev-update/index.html</span></a></p><p><a href="https://discuss.systems/tags/TLAplus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TLAplus</span></a></p>
Andrew Helwer<p>Reading the new experience report paper "System Correctness Practices at AWS" by <span class="h-card" translate="no"><a href="https://fediscience.org/@marcbrooker" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>marcbrooker</span></a></span> &amp; Ankush Desai, a successor to 2015 paper "How Amazon Web Services Uses Formal Methods". Documents a whole buffet of industrial formal methods use: P (including new tool PObserve for runtime trace validation), deterministic simulation testing in Rust with the open-sourced Shuttle and Turmoil tools, Dafny, HOL Light, and the open-sourced Kani model-checker for Rust.</p><p>While TLA⁺ was the most prominent featured tool in the 2015 paper, it's been lost in the crowd here as part of a clear shift toward verifying &amp; testing the actual running code. I think TLA⁺ must carve out a niche for itself in a world where deterministic simulation testing becomes a commodity technology, or it risks losing relevance same as other design-level tools like UML. There are existing case studies on using TLA⁺ for trace validation and model-driven testing, but a lot of effort needs to go into tooling for making such integrations as smooth as possible instead of bespoke one-off projects.</p><p><a href="https://dl.acm.org/doi/10.1145/3712057" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">dl.acm.org/doi/10.1145/3712057</span><span class="invisible"></span></a></p><p><a href="https://discuss.systems/tags/TLAplus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TLAplus</span></a> <a href="https://discuss.systems/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FormalMethods</span></a></p>
Andrew Helwer<p>I've really been enjoying work this month! The mission is to tag all ~200ish error checks in the TLA+ semantic parse layer with a unique error code, then come up with source code triggering that error. It's a very amusing sort of puzzle to look at a piece of code then try to reverse-engineer an input that will hit that branch while evading all previous checks. The lesson here is that for parsers, writing tests for code that should be accepted is boring - but writing tricky tests for code that should be rejected is fun!</p><p><a href="https://discuss.systems/tags/TLAplus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TLAplus</span></a></p>
Andrew Helwer<p>Hillel Wayne has an interesting post here exploring "Rosetta problems" within the context of formal specification languages: simple standard problems for comparing different languages by looking at how each language solves each problem.</p><p><a href="https://buttondown.com/hillelwayne/archive/what-are-the-rosettas-of-formal-specification/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">buttondown.com/hillelwayne/arc</span><span class="invisible">hive/what-are-the-rosettas-of-formal-specification/</span></a></p><p><a href="https://discuss.systems/tags/TLAplus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TLAplus</span></a></p>
Andrew Helwer<p>I wrote a TLA+ development updates newsletter for the TLA+ Foundation! Learn about various events, publications, and what people have been working on in the community. Hope to make this a monthly thing.</p><p><a href="https://foundation.tlapl.us/blog/2024-12-dev-update/index.html" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">foundation.tlapl.us/blog/2024-</span><span class="invisible">12-dev-update/index.html</span></a></p><p><a href="https://discuss.systems/tags/tlaplus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>tlaplus</span></a></p>
Andrew Helwer<p>Spent some time figuring out why the TLA⁺ proof manager release bundles are so large. Turns out it's the Isabelle dependency including an alarming number of binary packages, including a full JDK and Haskell stack!</p><p><a href="https://github.com/tlaplus/tlapm/issues/181" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">github.com/tlaplus/tlapm/issue</span><span class="invisible">s/181</span></a></p><p><a href="https://discuss.systems/tags/tlaplus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>tlaplus</span></a></p>
Andrew Helwer<p>Leslie Lamport's new book "A Science of Concurrent Programs" has been sent to the publisher and the final draft is available for free as a PDF!</p><p><a href="https://lamport.azurewebsites.net/tla/science-book.html" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">lamport.azurewebsites.net/tla/</span><span class="invisible">science-book.html</span></a></p><p><a href="https://discuss.systems/tags/tlaplus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>tlaplus</span></a></p>
Andrew Helwer<p>I'm also reading an older post by <span class="h-card" translate="no"><a href="https://mastodon.social/@pressron" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>pressron</span></a></span> called TLA+ in Practice and Theory (<a href="https://pron.github.io/posts/tlaplus_part1" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">pron.github.io/posts/tlaplus_p</span><span class="invisible">art1</span></a>). It does have one quote that I think is kind of funny:</p><p>&gt;Lamport observes that programming languages are complex, whereas ordinary, classical math is simple. Programming languages need to be mechanically translatable to efficient machine code that interacts with hardware and operating systems, and they are used to build programs millions of lines of code long that then need to be maintained by large and ever-changing teams of engineers over many years. Such requirements place constraints on the design of programming languages that make them necessarily complex, but this complexity is not necessary for reasoning about specifications;...</p><p>The bulk of my TLA+ tooling-related work for the past few years has been related to how to parse it, and MAN is it a complicated language to parse! So at least at that level I think most programming languages are simpler than TLA+. They are often designed with an eye toward parse simplicity.</p><p><a href="https://discuss.systems/tags/tlaplus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>tlaplus</span></a></p>
Andrew Helwer<p>I read a post by <span class="h-card" translate="no"><a href="https://hachyderm.io/@norootcause" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>norootcause</span></a></span> about prophecy variables. It does a very good job of demonstrating the need for them. I also think it's funny that, like mathematicians, computer scientists enjoy coming up with unrealistic pathological examples to disprove widely-believed principles (in this case using a queue with countably infinite length). Like a lot of my blog posts it builds up to a big crescendo before realizing that actually explaining the really hard part would double the length of the post, so the readers should just look at the explanation elsewhere. Still a good post and I came away from it with a blurry idea of how I would do the hard part anyway! <a href="https://surfingcomplexity.blog/2024/09/22/linearizability-refinement-prophecy/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">surfingcomplexity.blog/2024/09</span><span class="invisible">/22/linearizability-refinement-prophecy/</span></a></p><p><a href="https://discuss.systems/tags/tlaplus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>tlaplus</span></a></p>
Andrew Helwer<p>I wrote a blog post about how TLA⁺ is more than a DSL for breadth-first search - two other ways of looking at it, and what they could mean for any language wanting to be its successor!</p><p><a href="https://ahelwer.ca/post/2024-09-18-tla-bfs-dsl/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">ahelwer.ca/post/2024-09-18-tla</span><span class="invisible">-bfs-dsl/</span></a></p><p><a href="https://discuss.systems/tags/tlaplus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>tlaplus</span></a></p>
julia ferraioli<p>Gems from TLA+ Community Day:</p><p>"Formal mathematics is nature's way of letting you know how sloppy your mathematics is." — Leslie Lamport</p><p>"Animation and visualization is nature's way of letting you know how sloppy your formal mathematics is." — Michael Leuschel</p><p> <a href="https://floss.social/tags/FM2024" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FM2024</span></a> <a href="https://floss.social/tags/TLAPlus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TLAPlus</span></a></p>
Andrew Helwer<p>OpenSSH has a CVE caused by a race condition. Maybe I'll look at specifying that subsystem in TLA+ to see whether it can reproduce the bug. Of course since we know where to look and what details to focus on, specifying this doesn't give very strong evidence for a statement like "TLA+ would have found/prevented this bug" but at least it would be a fun side project!</p><p><a href="https://discuss.systems/tags/tlaplus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>tlaplus</span></a> <a href="https://discuss.systems/tags/openSSH" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>openSSH</span></a> <a href="https://discuss.systems/tags/cve_2024_6387" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>cve_2024_6387</span></a></p>