The lightweight formal methods callout is a good one. Maintaining a suite of proptest[1] strategies alongside the codebase is not a very much larger investment than writing unit tests by hand, but the insights they provide due to extensive coverage and compact understandable failure cases are way better. And crucially this approach does align with normal software development practices.
> Maintaining a suite of proptest[1] strategies alongside the codebase is not a very much larger investment than writing unit tests by hand,
I actually generate a unit tests with LLMs a lot lately. They do a decent job and you can just ask it to be a little more exhaustive, test any edge cases it can think of, or instruct it to deal with specific ones. I know a fair bit about how to write good tests and the effort you can put in that. But LLMs can generate better tests than me way faster.
If anything, they are less likely to do a half-assed job of it than me because I tend to run out of patience doing repetitive tedious shit. This is a healthy trait to have for a software engineer: we are supposed to make stuff easier by automating it. If it feels repetitive, your reflex should be to write code to make it less repetitive. Documentation is the same. I generate that too these days and since it is so easy, I do it more often and sooner.
LLMs might trigger a minor revolution in the adoption of formal method verification. Generating a correct specification is a combination of tedious and probably relatively easy for an LLM given enough context like working code, documentation, and other hints as to what the thing should do.
I'd be a lot more likely to bother with that stuff if I can just let it generate specification and then briefly glance through them than if I have to spell everything out manually.
I think using Rust kind of signals that you care about correctness. It's compiler is probably the closest to proving your system is probably correct that you can get without resorting to formal methods. And probably a lot easier than trying to bolt on formal methods to languages that don't even use a compiler or explicitly specified types.
Property tests are informal tests of formal properties. They don't guarantee the properties hold, or that the formal properties are complete, but they exploit the existence of these formal properties.
Once you have formal properties, you can write property-based tests using them, and I wonder how much of the benefit of formal methods could be obtained just by doing this. It's another example of using increased computing power (testing) to substitute for expensive hand labor (proving theorems).
I'll also observe that even theorem proving systems benefit from a kind of property based testing. If there's a goal to prove the existence of a value satisfying some property, this is essentially a property based testing problem. Similarly, find a counterexample to a universally quantified formula (also an existential problem) can be used to prune off unproductive branches of a search tree.
There's something also in the UX dynamics. As a developer writing property based tests I'm encouraged to think much more carefully about system invariants, otherwise there's not much value added over unit tests. For anything nontrivial this entails building a model of the system and checking it against the system under test, like they did at AWS. So the decision to use this tool shapes how you think about the system--it makes you reason more formally about it rather than just winging it and writing tests to exercise the code.
The assertion is that they're lightweight formal methods. Or is the article (and the proceedings of SOSP '21 it links to) wrong?
EDIT: ah I see where there might be confusion--obviously a library for generating random test data and making assertions about code under test itself doesn't constitute anything like "formal methods" but the idea of using that library in the way described in the paper linked from the article does. But that's kinda always the thing about software libraries..
Not sure what exactly you mean by "necessary", but I feel like the entire field of mathematics would disagree. Proving statements about infinite domains has a very long tradition.
The notion of a proof and verification of a real-life software are almost completely disjoint.
Of course, if you are interesting in proving statement about abstractly defined constructs: infinity is no issue as your domain is uniform. In real-life, this is not the case.
[1] https://crates.io/crates/proptest