This sounds fabulous on paper. Are there any examples of moving unit tests to property tests? Are there examples for proving unreachability? Has anybody successfully managed to explain how this is applicable if you don't have a deep background in formal methods?
If we can't provide a pathway from where we are to a more formal world that is understandable to garden variety developers, it will remain an ivory tower occupation.
(And, in fact, things will get worse. Because in a world of LLM churnage, provable correctness becomes even more important)
> Are there any examples of moving unit tests to property tests?
A quick google didn't turn anything up, but gosh there must be. Property tests have been around for ages.
> Are there examples for proving unreachability?
Yeah I do this all the time even in Haskell with just GADTs. You can do it in Rust with ! Too.
> Has anybody successfully managed to explain how this is applicable if you don't have a deep background in formal methods?
Amateurs played around with Haskell and now Lean all the time. But I guess that is a "certain type of person". We'll see how this stuff goes mainstream over time. E.g. maybe someday Rust will get dependent types.
> If we can't provide a pathway from where we are to a more formal world that is understandable to garden variety developers, it will remain an ivory tower occupation.
>
> (And, in fact, things will get worse. Because in a world of LLM churnage, provable correctness becomes even more important)
Part B helps with A a lot. If people writing fancier types are better able to leverage LLMs, and get more productivity boost accordingly, the basic economics will push it mainstream.
After all, there's more demand for "equally bad software quicker", than "better software at the same speed". :)
Eh, I think it is hard to get around the need for maintaining software, no matter how "worse is better" you are.
> But making it more accessible might just trigger enough people's "I don't want to push out absolute garbage if I can avoid it" buttons.
Yes, there is that too. Simple love of the craft.
> That's why I was wondering if there are already mainstream-accessible examples/explanations. It seems your search yielded the same results mine did :)
Just keep watching Lean. Now it is dominated by pure math, but people will be writing more programs over time also.
If we can't provide a pathway from where we are to a more formal world that is understandable to garden variety developers, it will remain an ivory tower occupation.
(And, in fact, things will get worse. Because in a world of LLM churnage, provable correctness becomes even more important)