The dependent languages are interesting. But the theorem proving is not easy, and probably overkill for a lot of applications. Even for stuff like boundary cond

The dependent languages are interesting. But the theorem proving is not easy, and probably overkill for a lot of applications. Even for stuff like boundary conditions for binary search, which could be checked with Hoare logic, I usually handle by stealing the implementation from the Go standard library (so I don't have to think about it). Last year I did advent of code in Lean4. I had written a heap implementation that I didn't end up using. As an exercise, I went back and added proofs for my indicies and a termination proof. I got the termination proof down to `0 < 0` and realized that I had an off by one error (I'd used the math for a 1-based array with a 0-based array). My take-away was that this stuff can catch real bugs, but also that people are not going to do this stuff day-to-day. Maybe some equality saturation thing will make it possible for the compiler to sort out the proof in most cases. If the compiler can hit 80%, you could use it as a linter. (If you want something stricter, you can do totality checking but have escape hatches like Idris' assert_total / assert_smaller.) > Even though at the time I wanted xhtml to win the battle of structured formats for the web, in hindsight I now believe messy html 5 was the way to go. The structured vs unstructured thing is also interesting. I came to a similar conclusion years ago. I'd written some heuristics to pull recipes out of web pages, and also use embedded microdata on some pages. I found I got better results with my heuristics because of bad encoding of the structured data. E.g. a web site was missing entire ingredient blocks in their encoding because their process / data model didn't accommodate recipes with multiple ingredient blocks.