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 <a href="https://futureofcoding.org" rel="nofollow">https://futureofcoding.org</a> website.<p>Some of my favourite episodes of the podcast:<p>• Compassion & Programming: Glen Chiacchieri - <a href="https://futureofcoding.org/episodes/026" rel="nofollow">https://futureofcoding.org/episodes/026</a><p>• Exploring Dynamicland: Omar Rizwan -
<a href="https://futureofcoding.org/episodes/028" rel="nofollow">https://futureofcoding.org/episodes/028</a><p>• The Edges of Representation: Katherine Ye - <a href="https://futureofcoding.org/episodes/034" rel="nofollow">https://futureofcoding.org/episodes/034</a><p>• Samantha John of Hopscotch on Learnable Programming - <a href="https://futureofcoding.org/episodes/005" rel="nofollow">https://futureofcoding.org/episodes/005</a>
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.<p>Hillel Wayne - Beyond Unit Tests: Taking Your Testing to the Next Level - PyCon 2018
<a href="https://www.youtube.com/watch?v=MYucYon2-lk" rel="nofollow">https://www.youtube.com/watch?v=MYucYon2-lk</a>
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?
Has anyone also read this book: <a href="https://www.amazon.com/Modeling-Software-Finite-State-Machines/dp/0849380863" rel="nofollow">https://www.amazon.com/Modeling-Software-Finite-State-Machin...</a> ? 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.<p>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've written some comments about this interview on the TLA+ subreddit: <a href="https://old.reddit.com/r/tlaplus/comments/bc37db/future_of_coding_podcast_38_the_case_for_formal/" rel="nofollow">https://old.reddit.com/r/tlaplus/comments/bc37db/future_of_c...</a>
But first, a word from our sponsor.<p>(<i>"SK:
Before I bring you Hillel, a quick message from our sponsor."</i> That's actually in the article.)