Jayaprabhakar

@JoeMaristela Oh boy... Rust and Python are just syntactic sugar for the same old 0s and 1s...

Another sanctimonious sermon on formal specs as "sets of behaviors" — just another a masterclass in stating the fucking obvious while pretending it’s profound. They wax poetic about how specs aren’t programs—bravo, rediscovering what every comp sci undergrad learns in week one. Meanwhile, you name-drop @Amazon’s #Kiro like it’s the second coming, yet conveniently ignore that their AI-driven spec tool is just another overhyped #FAANG cog, no better than the TLA+ you subtly diss for not being "programmer-friendly." Newsflash: your beloved FizzBee and P are just syntactic sugar for the same old formal methods, repackaged for hipster coders chasing #InnovationWankery. #TechBrosRediscoverMath / Seriously though, this is a decent read: buff.ly/WSOeR9E

@arundsharma @sunbains @ziglang @golang With that mapping, since we have the complete state transition from FizzBee spec, we can create exhaustive tests for transition coverage for single threaded tests, and also extensive concurrent (unlike manually created tests or other AI generated automated tests) tests.

@arundsharma @sunbains @ziglang @golang At a high-level, we need to provide some information on how the implementation implements the spec. That is, mapping for the actions like write, rotate etc to the code (classic Adaptor pattern) and mapping the state variables.

I've been trying to improve my Rust skills and learn more about formal specification this week, among other things. Today was my first foray into a real TLA+ specification. I cheated a bit, first I wrote the code and then with the help of Claude wrote the TLA+ specification. After some to and fro with the TLA+ checker I think it's quite good for a first attempt 😀. Not that I know any better. You can find the code and spec at: github.com/sunbains/wal

@arundsharma @sunbains If your using FizzBee, we can generate tests automatically to verify the implementation - at present FizzBee generates tests only for Go. Rust support is still in the works, though.

@sunbains What if the Rust code and TLA+ spec diverge? I'm aware of some efforts to do formal specs and proofs in Rust. But I'm skeptical because of the large surface area.

South Bay Systems Meetup: Replace TCP in the Datacenter @Yugabyte office. With JP author of FizzBee and John Ousterhout.

New blog post: surfingcomplexity.blog/2025/03/09/pax…

@devin_plumb Thanks @devin_plumb I'm glad you liked it.

This was an excellent lecture. Solving for reliability, error resilience, data integrity, etc is more important than ever and FizzBee is a much easier specification language for Python programmers than TLA+ or others Check it out here: fizzbee.io

Man this is awesome. I just did an episode with @jayaprabhakark and doing an episode on #slatedb. Connecting dots feels great.

When fizzbee.io finds a bug in slatedb.io's writer fencing protocol. 😵‍💫 github.com/slatedb/slated… /ht @vigneshc and @jayaprabhakark for this

Wonderful conversation with you @criccomini.

New post! I talk with JP about FizzBee, TLA+, and writing stable software. This one’s got me thinking about FizzBee + DST/Antithesis. materializedview.io/p/fizzbee-tla-…

FizzBee is a python-like language to model distributed systems and algorithms and prove correctness. From the model, you can now generate beautiful visualizations. fizzbee.io/tutorials/visu… #fizzbee #tlaplus #formal_methods #systemdesign #distributedsystems

Introducing FizzBee visualizations fizzbee.io/tutorials/visu…. You can now generate interactive sequence diagrams and whiteboard visualizations from design specifications.

The first post in my “Understanding Apache Iceberg’s Consistency Model” is out. This post covers the internals of the read and write path, details on metadata manipulation, concurrency control, and so on. If you ever wanted a more in-depth post about Iceberg internals, this is for you. jack-vanlightly.com/analyses/2024/…

5/5 Introducing FizzBee. Unlike other formal methods tools, this is specifically designed to be easy to use by software engineers. It uses Python's syntax, and has a powerful model checker with great visualization. Try now with an online playground at fizzbee.io

4/5 Every introductory blog on TLA+ will comment, "why do this instead of just writing in Python?" and explain the power of model checking in formal methods. Why can't we have the simplicity of Python AND the model checking power of TLA+? #tlaplus #Python

3/5 They all use 'Formal Methods'. If you work in any of these popular companies but never heard of formal methods, it's because only a small group of researchers or scientists use it. The current popular tool is TLA+ #TLAplus that is too complex to use for most engineers.

2/5 How do cloud service providers like #AWS, #AzureCosmosDB , #Mongodb , #Confluent, #ElasticSearch, ... validate there is no data loss or data corruption in their distributed systems? #DistributedSystems #SoftwareArchitecture #FaultTolerance #Microservices #SystemDesign

1/5 Every developer knows system design is crucial, but how do we validate our design is correct? How do we ensure the micro-services based cloud-native architecture is fault-tolerant and guarantees eventual consistency? How do we ensure there is no data corruption? #systemdesign