The Case for Formal Methods | Hacker News Reader

The Case for Formal Methods

futureofcoding.org

117 pointsstevekrouse17 comments

Steve Krouse's Future of Coding project is a fantastic resource for people working on programming languages, systems, editors, and other tools-for-making-our-tools. I heartily recommend anyone interested in the space spend some time poking around the https://futureofcoding.org website.

Some of my favourite episodes of the podcast:

• Compassion & Programming: Glen Chiacchieri - https://futureofcoding.org/episodes/026

• Exploring Dynamicland: Omar Rizwan - https://futureofcoding.org/episodes/028

• The Edges of Representation: Katherine Ye - https://futureofcoding.org/episodes/034

• Samantha John of Hopscotch on Learnable Programming - https://futureofcoding.org/episodes/005

I'm going to piggyback of your comment, since you're commenting on the website itself:

Is there any way to download this podcast for offline listening? I'm looking for podcasts I can listen to while driving without killing my mobile data quota.

If you are on Android, Google Podcasts and Podcast Addict both let you download the episodes.

The podcast should be available in any podcast player — just use the podcast player's search feature. I use the Overcast app for iOS and recommend it.

I found this talk (by the same person being interviewed) to be concise and convincing on how to do better than typical practice, without going to full formal methods.

Hillel Wayne - Beyond Unit Tests: Taking Your Testing to the Next Level - PyCon 2018 https://www.youtube.com/watch?v=MYucYon2-lk

I've been hearing about formal methods and provable specifications as long as I've been programming (which is going on 30 years now), and I remain skeptical about them. This sort of thing appeals to me - I've skimmed over TLA+ and I like the appearance of mathematical formalism (after all, I spent 6 years getting a master's degree in CS, it would be nice if I could ever actually apply any of it for once), but all the examples I've ever seen take up an incredibly long amount of time to specify/prove things that are actually... ridiculously trivial, like a FIFO. Now it's entirely possible that there's something really significant here, and I just haven't invested the time to dig down into this enough to understand it, but I feel the same way about React, and it seems like everybody on the planet has spent the time and effort making sense of React and has found it worthwhile - so why doesn't anybody else seem to be applying formal methods?

You might just not be hearing about what's happening in this area. Off the top of my head, formal tools are being applied at Microsoft (slam, everest, sage, Z3, ...), at Amazon (AWS security), at Netflix (tla+), at numerous hardware companies (Intel, AMD), at EDA vendors like Cadence and Synopsys, in avionics (DO-178C), and of course in academia (CompCert, L4 verified kernel, ...). I'm probably missing a lot.

Has anyone also read this book: https://www.amazon.com/Modeling-Software-Finite-State-Machin... ? I've actually stopped at 56% or so when it starts plugging their proprietary solution as mentioned in one of the reviews, the previous part being the theory of it, I very much enjoyed it though.

I had not learned about automata theory and electric engineering formal methods before, so I'm still trying to piece it together, seeing if I can fit this to my work and such, seemed very promising and kind of a "missing piece" in the puzzle to me. In that it seems to really allow to better model system behavior in a way that potentially could bind it to a spec, give new tools for seeing blindspots, etc, at the same being abstract enough that you could capture much with actions, control values, conditions and states.

I'm not sure about that book however this one: https://www.amazon.com/Practical-UML-Statecharts-Event-Drive...

got on my reading list by virtue of the misfortune of dealing with code written by programmers who adopted the book's approach.

The thesis was that state machines are a powerful formalism that can be fully verified because all the states and edges between them are known. That's half-right: they are powerful because state transitions are essentially "goto" by another name. In practice goto-based programming is brittle to requirement change. The damning part is that state machines don't live in isolation: they interact asynchronously with other state machines and the world at large. The dynamic behavior of these interactions is probably important! and not part of individual state machines. You'd need to co-simulate them.

I feel state machines have their place where no higher-level construct (usually I prefer coroutines) fits the job and it can be kept small and rewritten on requirement change.

That's interesting.. Well I've been thinking of how well would they work along with a rich domain model and high level programming in general.. The book also has a chapter on systems of state machines, one of the suggested approaches was of an hierarchical model in which the lower stms input the higher ones only through their states.. Was the project you talked about embedded sw? BTW UML is also criticized by the book I mentioned, so hopefully it's not the UML trap again :P

I've written some comments about this interview on the TLA+ subreddit: https://old.reddit.com/r/tlaplus/comments/bc37db/future_of_c...

this guy needs to formally verify his explanations. they are pretty weasly and convoluted. not sure anything of value in this

"Please don't post shallow dismissals, especially of other people's work. A good critical comment teaches us something."

https://news.ycombinator.com/newsguidelines.html

But first, a word from our sponsor.

("SK: Before I bring you Hillel, a quick message from our sponsor." That's actually in the article.)

Just like almost every podcast ever. It's a transcript of a podcast and so not surprising.

I'm just thankful they posted a legit transcript of the podcast at all! I don't like having to listen to them.

And you had to point this out why?

Reply on news.ycombinator.com