Lightnews — Scholar-powered news

Mike Dodds

@m-dodds.bsky.social

210 followers 55 following 55 posts

Formal methods nitwit. https://mikedodds.github.io

AI / math / formal methods paper feed: @ai-fm-papers.bsky.social

Posts Replies Media Videos

Mike Dodds

@m-dodds.bsky.social

New Galois blog: “Specifications Don’t Exist”. If we want to formally verify more systems, we need formal specifications, but most real systems are hard to specify for very deep reasons www.galois.com/articles/spe...

Screenshot of article text: “Formal verification today is very useful, but for most systems it’s very difficult to write the kinds of complete specifications that verification needs. However, other kinds of specifications are popular: for example, a test case is a kind of limited, partial specification. The key is that a test case is immediately useful, and doesn’t impose undue costs on the development team. We need to find ways to specify systems that have these virtues, and avoid the trap of imposing a complete and coherent view that fundamentally does not exist.”

Screenshot of article text: “ I’ve come to think writing formal specifications is just a very difficult task. It requires a top-down view of the system that designers and engineers typically don’t have or, more importantly, need. In contrast, informal specifications can be ambiguous, partial, flexible. Informal specifications are intended as communication mechanisms between humans, and as a result they can be ‘wrong but useful’, and elide aspects of the system that are not of interest. This is a strength, but it also results in systems that can’t be easily formalized.”

Screenshot of article text: “ I think systems are typically both designed from the top and grown incrementally. Most systems have some degree of top-down structure, but few systems have a mathematically coherent specification that covers every behavior. The effect is that most systems obey some formal specification for some core functionality, but if outside this core, we rapidly enter muddy territory where it is unclear what the system should do, or whether the designer should even care”

Screenshot of article text: “ It’s a formal verification cliché that writing the specification tends to uncover most of the bugs in a system. To me, this suggests an analogy between specification and programming—both are tools for expressing what we want. In one way, this is a pessimistic thought: no tool can remove the burden of clarifying our ideas. But also, it gives me some hope. Programming is very difficult, but through careful tool design, we’ve made it available to hundreds of millions of people. With luck and skill, perhaps we can do the same for specifications.”

July 16, 2025 at 12:48 AM

Mike Dodds

@m-dodds.bsky.social

If a tool is not popular, it’s uncompelling to argue that everyone is just mistaken. At some point you should ask why the tool isn’t useful (at the current cost/benefit point)

Text screenshot: I sometimes hear people claiming that formal methods are demonstrably better than the techniques software engineers mostly use today. The only reason formal techniques aren’t more popular (according to this theory) is that engineering teams are unaware, conservative, maybe put off by superficial difficulties like poor interfaces and documentation. I don’t think this is quite right. My observation is that engineers are mostly rational when thinking about costs and benefits, at least within the bounds of their particular systems and problems.

May 24, 2025 at 2:12 AM

Mike Dodds

@m-dodds.bsky.social

New-ish @galoisinc.bsky.social blog: “What Works (and Doesn't) Selling Formal Methods”. The boring truth: engineers are rational and adoption is all about cost/benefit tradeoffs www.galois.com/articles/wha...

A graph of costs and benefits plotted against each other. There is a line under which is “Your favourite under-appreciated formal method”. There are two arrows pointing orthogonally away: “be cheaper” and “be more beneficial”

May 24, 2025 at 2:12 AM

Mike Dodds

@m-dodds.bsky.social

I’m bringing these cute Galois stickers to POPL so if you want one, come find me

January 20, 2025 at 8:09 PM

Mike Dodds

@m-dodds.bsky.social

A big jump on coding skill as well:

December 21, 2024 at 5:19 PM

Mike Dodds

@m-dodds.bsky.social

Re o3 - this is the big one for me. The Frontier Math benchmark is designed to be extremely difficult, and it has a private test set (no data contamination).

Today, o3 is v expensive. But seems inevitable it’ll soon be cheap. If these results hold up, that means MUCH more powerful automated math

December 21, 2024 at 5:19 PM

Mike Dodds

@m-dodds.bsky.social

I think specification will be a much harder problem. Nearly all successful proof deployments have been in “easy to specify” domains - OSs, hardware, crypto, etc. these are unusual, & most systems are very difficult to specify formally

December 17, 2024 at 3:10 AM

Mike Dodds

@m-dodds.bsky.social

Optimistically this could haul a lot of tools across the break-even line into viability. There are many formal methods ideas that simply haven’t been tried because the cost/benefit never worked out. Exciting times for proof tech / FM

December 17, 2024 at 3:10 AM

Mike Dodds

@m-dodds.bsky.social

I think there’s good reason to be optimistic that proofs themselves will get much cheaper. Most proof tools are structured as untrusted search and trusted checking. Gen AI is a just new untrusted search process which should slot right in alongside SMT solving etc

December 17, 2024 at 3:10 AM

Mike Dodds

@m-dodds.bsky.social

I gave a talk recently about proof technologies - what people deploy today, what might be available soon, and what seems far off even with fancy AI. Slides here: mikedodds.github.io/files/talks/...