infer VS Error Prone

Meta/Facebook are long time OCaml users, their logo is on the OCaml website. Their static analysis tool and its predecessor are both written in OCaml.

Efforts: Dependabot, CodeQL, Coverity, facebook's Infer tool, etc

I notice there isn't fbinfer. It's pretty cool, and is used for this library.

TBH, there's a non-zero amount of non-"ivory tower" tools you may have used that are written in functional languages. Say, Pandoc or Shellcheck are written in Haskell; Infer and Flow are written in OCaml. RabbitMQ and Whatsapp are implemented in Erlang (FB Messenger was too, originally; they switched to the C++ servers later). Twitter backend is (or was, at least) written in Scala.

- borrow-cpp which exploits some null dereference checks in the infer static analyzer to model some of borrow checking.

> Maybe you could write tests as queries that would test a whole set of possible programs, not only the current version of your program at the moment.

I think that the future of programming is more sophisticated static analysis. Programmers will write statements like, "every code path that writes to the Payments database must have called validate_user()." Then, the tooling will confirm that rule with every commit.

We kind of have this already (for example, Facebook's Infer tool [0]), but I think it will become much more important in the coming decade.

0: https://github.com/facebook/infer

Great question! Formal methods groups in industry are growing rapidly and popping up in surprising places. Amazon's group is probably the most famous, but I think pretty much every big tech company has something going on in the formal verification / static analysis space. There's also a lot going on in blockchain . It's definitely becoming harder to hire people with FM skills, so in that sense, I think it's a great space to get into.

The downside is that the space is quite fragmented and a lot of tools have a high skill bar. If I was starting out, I'd probably focus on static analysis (eg. Infer or something similar - https://github.com/facebook/infer) because those tools tend to be easier to learn, and they have the potential to scale to really big systems. In contrast, Coq is a fine tool, but most people learn it by going to grad school which isn't useful short term career advice.

There are lot of great interviews with practitioners on the Galois podcast, Building Better Systems - that might be a good place to start exploring: https://www.stitcher.com/show/building-better-systems

> The only reliable way to have bug-free code is to prove it. It requires solid mathematical foundations and a programming language that allows formal proofs.

I'm going to be the "actually" guy and say that, actually, you can formally verify some studff about programs written in traditional/mainstream languages, like C. Matter of fact, this is a pretty lively research area, with some tools like CBMC [0] and Infer [1] also getting significant adoption in the industry.

[0]: https://github.com/diffblue/cbmc

[1]: https://fbinfer.com/

error-prone is good for some extra static analysis.

A special kind of validation is enforcing that record fields are not null. (Un)fortunately, records do not have any special behavior regarding nullability. You can use tools like NullAway or Error Prone to prevent null in your code in general, or you can add checks to your records:

I am all in favour to more third side libraries adding functionalities, like Lombok, Manifold and error prone. As well as smaller projects like this shameless plug and what appears in this list

If only Google didn't suck when it came to Java9+ support... https://github.com/google/error-prone/issues/2649

I haven't used it. I use Google's ErrorProne + Lombok to prevent NPEs in java.

Take a look at NullAway, a plugin for Error Prone.

While at it you could also point them to static code analyzers such as error_prone, spotbugs and pmd (use all 3 at once - they complement each other in detecting different issues).

5. Error Prone