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

[@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.