Joined 14 years ago
"The agent can read full file contents, search the codebase, inspect other changed files for context, and produce deep reviews — not just surface-level diff feedback." our tool does all this too. It catches dumb typos as well as more complicated bugs. Not to mention it is great as a ratchet (https://qntm.org/ratchet). It is not a substitute for reviews from other engineers though, since obviously it does nothing to achieve one of the main goals of code review, which is to socialize knowledge of the codebase.
Alibaba's work here is almost certainly more advanced than what we've done, but ours has been perfectly satisfactory and better than the paid offerings we've tried. I think most teams should not be paying SaaS fees for AI code review, that is the kind of business that mostly should not exist any more.
"Meta’s own researchers found — in an experiment they believed was better designed than any external study done thus far — that reducing time on their platforms improved mental health and well-being, specifically depression, anxiety, loneliness, and social comparison."
I am what the article calls an "industrial software engineer" and I work on "low- to medium-assurance" projects, but have used various formal methods (alloy and TLA+) in my work to prevent and discover bugs.
I've experimented with using LLMs to generate both Alloy and TLA+ a couple times over the past years, and the problems I see are:
- They have gotten better over the last few years, but still can only produce useful results in the hands of someone who is moderately competent. Becoming moderately competent requires many hours of investment in these tools, and you will lose much of this competence if you don't keep it up. For example, I can still read TLA+ and Pluscal but can't write them without lots of referring to the docs because I only write them like once or twice a year.
- They suffer even more from GIGO than other aspects of software development. If you can't really rigorously define your problem you will get a bad model/output that only gives you false confidence. A large part of the value of doing formal methods is building the muscle for thinking rigorously. Hillel Wayne says this in several places, that doing enough TLA+ (e.g.) work gives you a much better innate sense for where there will be race conditions.
- There will still be a cultural and technical problems with integrating formal methods, and their artifacts, into the rest of your codebase and team. For example, how do you prevent drift? Will you have a CI automation that uses an LLM to detect when the spec has diverged from the code?
I'm not saying it is impossible that this will happen, and I would love to be wrong, but the general tendency I see with LLM use is to make software developers less intimately familiar with their tools, and less invested in deeply understanding their code. That bodes ill for formal methods even more than regular programming.
