"Can a Programming Language Reason About Systems?" by Marianne Bellotti (Strange Loop 2023)

We have lots of languages that apply logic to verifying, simulating, or generating systems, but they all use the syntax of mathematical proofs which many programmers find difficult to learn. Fault is a new language developed to help people model systems and reason about their behavior and limitations. These systems can be technical, they can be organizational, regulatory or they can be hybrids. This talk will cover the basic styles of logic programming-model checking, simulation, symbolic execution-and how Fault converts a programmer friendly syntax into logic friendly models. Watch Fault do things like give advice about 5,000 page export regulations, tell you when your micro services architecture is going to start breaking down, and solve sudoku puzzles.
Marianne Bellotti
Rebellion Defense
@bellmar
Marianne Bellotti is the author of Kill It With Fire, Building Safety Critical Systems, and Hiring Engineers, as well as a popular column on technology and system safety. She has built data infrastructure for the United Nations to help humanitarian organizations share crisis data and tackled some of the oldest and most complicated computer systems in the world as part of United States Digital Service. At Auth0 she ran Platform Services, a portfolio that included shared services, untrusted code execution, and developer tools. Currently she runs engineering teams at Rebellion Defense. She can be found on most social networks under the handle bellmar.
----
Recorded Sept 22, 2023 at Strange Loop 2023 in St. Louis, MO.
thestrangeloop.com

[@ytpah9823]

🎯 Key Takeaways for quick navigation:
00:50 🎉 Marianne Bellotti expresses gratitude to Alex and the team for running Strange Loop for over 10 years.
02:12 🛠️ Formal methods focus on proving system correctness, but in legacy systems, it's often more about understanding and improving the existing systems.
03:32 🤔 Understanding how people become experts in systems is crucial for improving system understanding and knowledge transfer.
04:16 🧠 Experts build mental models of systems based on their experience and observations, helping them deduce system behaviors and potential issues.
05:00 🔍 Building mental models typically occurs through operating systems and incidents, allowing experts to learn more about system behavior.
06:25 🤯 A mental model is a pattern used as an analogy to understand and analyze complex systems and their interactions.
07:07 🤖 Formal methods can help communicate and formalize these mental models and abstractions.
09:11 🔄 Symbolic execution involves modeling system behavior using variables and relationships, which helps verify and understand complex systems.
14:12 🆚 Fault is a domain-specific language that aims to provide an accessible way to express and communicate models for systems.
15:07 🛠️ Fault compiles down to smt lib 2 and focuses on enhancing expressiveness for modeling systems.
21:56 🧪 The stock-flow model is used to represent feedback loops in systems by considering resources (stocks) and functions (flows) that affect them.
22:22 🧰 Fault, a programming language discussed in the video, defines abstractions, stocks, flows, and connections to model systems.
23:05 🔄 Fault is a bounded loop model, which means it runs for a specific number of rounds, following defined steps to validate constraints.
23:47 📝 Single Static Assignment is used in compilers and helps maintain the immutability of variables by creating new variables when their values change.
26:02 🔀 Fault uses Polish notation, a change in operator order, to handle parallel processes like the System Dynamics bathtub model.
27:25 💡 Phi values in single static assignment help normalize variables when branching logic is involved, keeping counts synchronized.
28:06 📊 Fault's output from SMT solvers can be challenging to read due to unordered results and occasional expressions.
30:22 🛠️ Marianne Bellotti explores various methods of interpreting and visualizing the results to make them more user-friendly.
31:44 🤖 Fault can express string manipulation as boolean logic, making it easier for humans to understand and interpret rules.
33:09 📜 Using static rules to check policies, such as federal employee vaccination requirements, can reveal unusual scenarios and edge cases.
36:11 🕰️ Fault can handle time-based scenarios by using the stock-flow construct, defining conditions for transitioning between states.
38:28 📊 Modeling dependency graphs and boolean lattices in Fault can help represent project dependencies and ensure correct behavior.

[@5pp000]

Very interesting talk! As we find ways to offload more and more of the work of writing actual code to our machines, we are going to need better ways to tell them what we want them to do than just trying to describe it in natural language, with its vagueness and ambiguity. Formalisms like these will become more important.

[@blaiseutube]

This may be the single most important question.