Different methods find different things. Personally, I'd rather use a language that is memory safe plus a great static analyzer with abstract interpretation that can guarantee the absence of certain classes of bugs, at the expense of some false positives.
The problem is that these tools, such as Astrée, are incredibly expensive and therefore their market share is limited to some niches. Perhaps, with the advent of LLM-guided synthesis, a simple form of deductive proving, such as Hoare logic, may become mainstream in systems software.
>> Also Claude owes its popularity mostly to the excellent model running behind the scenes.
It's a bit of both. Claude Code was the tool that made Anthropic's developer mindshare explode. Yes, the models are good, but before CC they were mostly just available via multiplexers like Cursor and Copilot, via the relatively expensive API.
It should be better for the reasons explained in the article. Pure functions require no context to understand. If they are typed, it's even simpler. LLMs perform badly on code that has lots of state and complex semantics. Those are hard to track.
In fact, synthesis of pure Haskell powered by SAT/SMT (e.g. Hoogle, Djinn, and MagicHaskeller) was already of some utility prior to the advent of LLMs. Furthermore, pure functions are also easy to test given that type signatures can be used for property-based test generation.
I think once all these components (LLMs, SAT/SMT, and lightweight formal methods) get combined, some interesting ways to build new software with a human-in-the-loop might emerge, yielding higher quality artifacts and/or enhancing productivity.
That's a very fair point. There are some publications showing lower performance for languages with less training data. I imagine it also applies to different paradigms. Most training code will be imperative and of lower quality.
I think LLMs are great at compression and information retrieval, but poor at reasoning. They seem to work well with popular languages like Python because they have been trained with a massive amount of real code. As demonstrated by several publications, on niche languages their performance is quite variable.
This is very impressive, top labs doing research often don't have experimental designs that are this elaborate. Was the TCR and BCR-seq you conducted helpful to design cell therapies, neoantigen vaccines, and monitor progress?
Given that you carry the HLA-B*27:05 allele, you might have been blessed by being predisposed to a better response. But probably you want to keep an eye on future autoimmunity issues. Talking from experience...
Thanks for the warning, I hope that it wasn't a personal experience for you.
Thanks for the compliment about the elaborate design. I think that when you make something for one or a few patients it is easier to be more elaborate, even with the same knowledge and equipment.
Maybe the TCR and BCR-seq was most helpful for mRNA design and effectiveness monitoring, but hopefully someone else on my team will answer that better.
The TCR sequencing has been helpful for downselecting TCRs for a TCR based cell therapy, and for monitoring response to various immune therapies (including the vaccines)
reply