r/programming • u/1_more__user___name • 22h ago

Building confidence in concurrent code with a model checker - Scott Wlaschin - NDC London 2023

https://youtu.be/qs_mmezrOWs?is=v3oxPNQ4EFSdwgZ6

I have followed Scott for some time because of his contributions to the fsharp learning community. He's website fsharpforfunandprofit.com is one of the best programming article websites. This talk especially is very good. I think Scott is very good at breaking down complex topics to make them seem approachable.

21 Upvotes

85% Upvoted

7 comments sorted by

8

u/pobbly 16h ago

Finding TLA+ and more recently Quint indispensable for anything serious these days!

3

u/Boukhaaa 16h ago

Quint is just great! So easy to read and the CLI style tooling makes integrating it into my agentic workflows so simple.

1

u/1_more__user___name 15h ago

I'm new to model checking. Do you apply it to domains other than concurrent code?

1

u/Boukhaaa 14h ago

Quint is a specifications language, the verification and model checking are just part of the advantages of these tools and it applies best to distributed and concurrent systems. I use Quint mostly to formalize my requirements into executable specs and that helps me have a better understanding of what I am trying to build especially when agents are the ones doing the programming.

1

u/1_more__user___name 11h ago

Don't you still have to verify that the LLM translated the specs to code correctly? Can Quint help with that? To me TLA+ is solving an existing problem that exists with or without LLMs, that your model is correct. 

1

u/1_more__user___name 15h ago

Do you apply it to anything other than concurrent coding?