Hillel Wayne
Writer and consultant on formal methods, testing and software correctness, author of Logic for Programmers and Practical TLA+. He ran the Crossover Project, interviewing seventeen people who worked as traditional engineers before becoming software developers, to settle by evidence whether software engineering is engineering.
Hillel Wayne did not write this page.
We collected these quotes from things they published elsewhere, and every quote links to where it was said. They have no account here and have not endorsed this site. Quotes are word for word; the short line under each one is our own restatement, not their wording. Their own site. Is this you? Claim it or ask us to remove it. Or tell us what is wrong here.
-
Their wordsIf I had to summarize what I found in general, I'd put it like this. Everybody hates waterfall.
↗Formal methods with Hillel Wayneyoutube.com 1st of 24 in this recording
-
Their wordsThe core tension of engineering is between how expensive it is to make a mistake and how quickly you can iterate. The faster you can iterate, the less planning you need to do before you iterate, and the more expensive it is, the more planning you need to do.
↗Formal methods with Hillel Wayneyoutube.com 2nd of 24 in this recording
-
Our reading
Software did not invent iterative development: mining engineers had their Agile revolution in 1960.
Their wordsAnd the first thing he pointed out to me was that they had their Agile revolution in 1960.
↗Formal methods with Hillel Wayneyoutube.com 3rd of 24 in this recording
-
Their wordsSoftware is kind of unique in having the third kind of the practitioner conference where we are just meeting to get better at what we do. We also are really the only kind to really focus heavily on like open source in making our knowledge freely available.
↗Formal methods with Hillel Wayneyoutube.com 4th of 24 in this recording
-
Their wordsYeah, I interviewed like 20 people on this. I think all 20 mentioned version control as the thing they wish they had in their old field.
↗Formal methods with Hillel Wayneyoutube.com 5th of 24 in this recording
-
Our reading
Software iterates better than every other engineering field and plans worse than all of them.
Their wordswhile we are a lot better at iterating than other fields, we're worse at the planning part. Like we still need to do some kind of planning before we iterate and we just aren't as good as those other fields.
↗Formal methods with Hillel Wayneyoutube.com 6th of 24 in this recording
-
Their wordsAnd that kind of compiling of information about the materials is something other fields do that we don't do. An analogy that I would think of in software would be something like a 500-page book on how to version an API.
↗Formal methods with Hillel Wayneyoutube.com 7th of 24 in this recording
-
Their wordsI think this project and writing about it and thinking about it has firmly moved me from the camp of we are definitely not to we probably are.
↗Formal methods with Hillel Wayneyoutube.com 8th of 24 in this recording
-
Their wordswhen you start talking about like most interesting domain problems, you have to pull in so much context that basically even writing what the function is supposed to do becomes a nightmare. The imperative program you write that will get correct 99% of the time is probably good enough to use in almost all cases.
↗Formal methods with Hillel Wayneyoutube.com 9th of 24 in this recording
-
Their wordsbut I can tell you with first hand experience nuclear power plants do not care about this stuff. They're actually just fine with with with thorough testing.
↗Formal methods with Hillel Wayneyoutube.com 10th of 24 in this recording
-
Their wordsThen the actual system might still have bugs, but we can iron out the issues in the abstraction such that we don't actually build them in the real system.
↗Formal methods with Hillel Wayneyoutube.com 11th of 24 in this recording
-
Their wordsI think a large part of the problem of why it's hard for us is because you don't get a lot of practice. Usually when you have a race condition in a system, you find out months later and then you try a fix and you find out weeks later after that if the fix actually worked.
↗Formal methods with Hillel Wayneyoutube.com 12th of 24 in this recording
-
Their wordsBut I think it is more useful for most developers to have an exposure to like what math has in the various fields versus just going all in every single field when they see them, right? You've got to know what's available to know what's most useful for you. And most math will not be useful for you.
↗Formal methods with Hillel Wayneyoutube.com 13th of 24 in this recording
-
Their wordsAnd I wonder sometimes if that is the reason people don't recognize the use of math in software engineering is because the math they do need is not the math they've been exposed to.
↗Formal methods with Hillel Wayneyoutube.com 14th of 24 in this recording
-
Their wordsI think the case of TLA+ and most, not all, but most formal methods, they shine the most in highly computational domains, where most of the problems are highly technical and not like business embedded.
↗Formal methods with Hillel Wayneyoutube.com 15th of 24 in this recording
-
Their wordsI think a lot of the reason people are skeptical of these is because they've been burned by things like case and UML and all these other miracle solutions that were forced on them by people who wanted them to use it no matter what.
↗Formal methods with Hillel Wayneyoutube.com 16th of 24 in this recording
-
Their wordsI love formal methods, but I think it's a fairly niche tool for most people and I think like property-based testing is in general going to be useful for more people.
↗Formal methods with Hillel Wayneyoutube.com 17th of 24 in this recording
-
Their wordsAnd often I found with my clients I have to tell them like it's doing a good job at generating the actual design, but in actually expressing what the design is supposed to do, it cannot do that yet. You have to do that part yourself.
↗Formal methods with Hillel Wayneyoutube.com 18th of 24 in this recording
-
Their wordsAs a general thing we've seen like to get good results you have to already know how to get good results without it. It just helps you get good results faster.
↗Formal methods with Hillel Wayneyoutube.com 19th of 24 in this recording
-
Their wordsI think it is making it more popular. I don't know if it'll make it go mainstream, but it's definitely making it a lot more popular. It's bringing it from maybe like 0.1% to 0.3% which is huge.
↗Formal methods with Hillel Wayneyoutube.com 20th of 24 in this recording
-
Their wordsSo, it's hard to tell how much of like the loss of the past few years was AI versus the end of like zero interest rate policy and like the post-COVID crash. And I think it's more the latter, but like again, LLMs are still getting better.
↗Formal methods with Hillel Wayneyoutube.com 21st of 24 in this recording
-
Their wordsI predict that in the next 10 years software development will survive, but it will become like any other white-collar professional work. No more $200,000 salaries, unlimited vacation, or incredible employee bargaining power.
↗Formal methods with Hillel Wayneyoutube.com 22nd of 24 in this recording
-
Their wordsAnd up until now that like could only really happen if one of those people in that family that community or that school was like really really into computers. But now it's possible for everybody to have situated software.
↗Formal methods with Hillel Wayneyoutube.com 23rd of 24 in this recording
-
Our reading
Nobody in software treats debugging as a discipline; it is left as a handful of basic heuristics.
Their wordsBut this is the book that I give to every junior engineer because I think like nobody ever really talks about debugging as like a discipline outside of like basic heuristics.
↗Formal methods with Hillel Wayneyoutube.com 24th of 24 in this recording
- 6 years earlier
-
Their wordsAlmost everything we think is unique about software appears in every other field of engineering.
-
Their wordsTo assume that software is uniquely unpredictable is a special kind of arrogance.
-
Their wordsPlenty would kill to get the same kind of automated testing we treat as a given.
-
Their wordsSoftware is far more consistent than any other kind of engineering.
-
Their wordsWe can change software much faster than anybody else can change their systems.
-
Their wordsRather than fix a trad issue with trad engineering, Boeing opted for the software kludge, and then people died.
-
Their wordsBut constraints in software tend to be soft constraints.
- 2 days earlier
-
Their wordsNone of the people arguing for or against software engineering as engineering have worked as engineers.
↗Are We Really Engineers?hillelwayne.com 1st of 6 in this piece
-
Their wordsJust because we use a different branch of math doesn't mean we're not doing engineering.
↗Are We Really Engineers?hillelwayne.com 2nd of 6 in this piece
-
Their wordsMuch of the engineering there is low-stakes, low-consequence, just like much software is.
↗Are We Really Engineers?hillelwayne.com 3rd of 6 in this piece
-
Their wordslicenses exist because we are part of society and have legal requirements, not because they are essential to what it means to do engineering
↗Are We Really Engineers?hillelwayne.com 4th of 6 in this piece
-
Their wordsOf the 17 crossovers I talked to, 15 said yes.
↗Are We Really Engineers?hillelwayne.com 5th of 6 in this piece
-
Their wordsWe are separated from engineering by circumstance, not by essence, and we can choose to bridge that gap at will.
↗Are We Really Engineers?hillelwayne.com 6th of 6 in this piece
- 24 months earlier
-
Their wordsmost people in high-assurance software don't use formal methods
↗Why Don't People Use Formal Methods?hillelwayne.com 1st of 5 in this piece
-
Their wordsFinding the right spec is one of the biggest challenges in formal methods.
↗Why Don't People Use Formal Methods?hillelwayne.com 2nd of 5 in this piece
-
Their wordsFormal verifiers have a dilemma: the more expressive the language, the harder it is to prove anything in it. But the less expressive the language, the harder it is to write anything in it.
↗Why Don't People Use Formal Methods?hillelwayne.com 3rd of 5 in this piece
-
Their wordsIn fact, the vast majority of distributed systems outages could have been prevented by slightly-more-comprehensive testing.
↗Why Don't People Use Formal Methods?hillelwayne.com 4th of 5 in this piece
-
Their wordsYou do not need full code verification to write good software or even to write near-perfect software.
↗Why Don't People Use Formal Methods?hillelwayne.com 5th of 5 in this piece
- 16 months earlier
-
Their wordsUncle Bob gives terrible advice. Following it will make your code worse.
↗Uncle Bob and Silver Bulletshillelwayne.com 1st of 3 in this piece
-
Their wordsRather, the best way to reduce the volume and severity of mistakes is to adjust the system itself.
↗Uncle Bob and Silver Bulletshillelwayne.com 2nd of 3 in this piece
-
Their wordsBut unit tests don't give you much confidence in your code.
↗Uncle Bob and Silver Bulletshillelwayne.com 3rd of 3 in this piece