This is such an interesting talk! However I think the take on EWD's contributions to computer science could use a different take. On maintainability and extens

This is such an interesting talk! However I think the take on EWD's contributions to computer science could use a different take. On maintainability and extension of systems it is possible to achieve a system like Sussman's propagators while still maintaining proofs of correctness. It's true that overly specific proofs that don't work on the more general principles are harder to maintain in step with a changing program; however the trade-off is that you don't know if the change you made (to the highly dynamic system) will have the desired effect (or at least, you can't prove it doesn't). For a small circuit diagram it might be simple enough that there are obviously no errors. However the prevailing approach to software development is to make software so complex there are no obvious errors. Biological systems seem to get around this by encoding a lot of redundant information, preserving a ton of errors, and it takes millions of years to sort them out. I think though that in some cases it does make sense to trade off some correctness when prototyping and experimenting with ideas. However, in my limited experience, taking that idea to the extreme can lead to systems that only the original author can understand. Mathematics may be impressionistic but the formalization of mathematics, though tedious and pedantic, isn't! It wouldn't be until a few years later when systems like Lean are shared to the wider world (and Coq continues to improve) that show how maintaining more general proof-level engineering can be done on a larger scale without sacrificing flexibility. Sussman is legendary. Loved this talk!