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:

363
active users

#tlaplus

0 posts0 participants0 posts today

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 & how the TLA+ Foundation has been funding work to overcome them, and what I'd like to see come next for TLA+!

youtube.com/watch?v=KrhZebeRn9

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.

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.

github.com/tlaplus/tlaplus/iss

GitHubSupport company-level execution statistics · Issue #1170 · tlaplus/tlaplusBy lemmy

Reading the new experience report paper "System Correctness Practices at AWS" by @marcbrooker & 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.

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 & 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.

dl.acm.org/doi/10.1145/3712057

QueueSystems Correctness Practices at AWS: Leveraging Formal and Semi-formal Methods: Queue: Vol 22, No 6 Building reliable and secure software requires a range of approaches to reason about systems correctness. Alongside industry-standard testing methods (such as unit and integration testing), AWS has adopted model checking, fuzzing, property-based testing, ...

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!

Replied in thread

I'm also reading an older post by @pressron called TLA+ in Practice and Theory (pron.github.io/posts/tlaplus_p). It does have one quote that I think is kind of funny:

>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;...

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.

Ron Pressler · TLA+ in Practice and Theory<br/>Part 1: The Principles of TLA+TLA+ is a formal specification and verification language intended to help engineers specify, design and reason about complex, real-life algorithms and software or hardware systems. We explore its motivation, application and principles of design.
Continued thread

I read a post by @norootcause 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! surfingcomplexity.blog/2024/09

Surfing Complexity · Linearizability! Refinement! Prophecy!Back in August, Murat Derimbas published a blog post about the paper by Herlihy and Wing that first introduced the concept of linearizability. When we move from sequential programs to concurrent on…

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!