Formal methods with Hillel Wayne

Hillel Wayne: The 'materials' in software engineering are freakishly consistent. All other engineering professions have to worry about the consistency of their materials; for example, electrical engineers work with resistors that offer resistance within 20% of 100 ohms across a thousand units, and only when operated within a given temperature range. In contrast, a program runs identically on any given computer in software engineering. Hillel argues that the variability we deal with in software, like versions, APIs, bugs with integrations, etc, are largely battles of our own making.

Hillel Wayne: It's because specs in the real world are a nightmare to write. Even a simple problem like 'find the file in a directory that has the most lines' gets complicated when modeled with formal methods. We would have to answer questions like: 'do we look at ASCII or UTF-8 new line characters, what about unreadable files, and Symlinks?' Without formal methods, we can write a simple verification that is right in 99%+ of cases. Formal methods require a lot of extra effort for the less than 1% of exotic use cases!

Hillel Wayne: Hillel recommends most engineers adopt property-based testing, and stop there. Property-based tests mean defining properties which the test then throws thousands of inputs at, in order to stress test a system. Hillel is convinced that formal methods are a niche tool for most engineers, whereas property-based testing is the most practical approach for building robust software with this lightweight formal method.

Hillel Wayne: AI won't make formal verification mainstream, but will increase its use. As Hillel says, 'AI bringing formal verification up from maybe 0.1% to 0.3% across the industry would still be huge!' He also finds that people who succeed at using AI to generate formal specs are often formal verification experts.