Do you also think that primary school students should not be taught, say, multiplication? Because they can, of course, use a calculator. No need to ask them what 3 times 4 is.
Having some experience in this field, I can say that all of the tools presented on the webpage are very lightweight static analyzers. They are all based on processing the syntax tree and they which will detect things like uninitialized variables, or do style checks.
"Real" static analyzers, which are more useful, are based on symbolic execution and abstract interpretation and they will uncover more interesting classes of errors, like double frees, out of bounds array access, etc.
Note that all analyzers will have FPs and FNs, because the underlying problem is uncomputable.
The best open source "real" static analyzer overall for C++ is the Clang static analyzer. There are many commercial analyzers available, and most C++ shops will use one or more of these.
To those wondering if there will be a successful "marriage" between popular incarnations of AI, like ChatGPT, and FM: no, at least not in the sense you would expect.
Sure, ChatGPT will successfully manage to find formal proofs that have been done before.
But synthesising proofs from scratch is NP-complete for the simplest proofs (or worse for more interesting cases), and LLMs are simply not clever enough to do it (except in cases where the proof has been seen before).
It could be possible to integrate an SMT solver with a LLM to make this work, but the core difficulty of the FM task will then be solved by the SMT solver.
I would like to point out that such a resource is useful for reference purposes (only).
If you want to really understand an algorithm/a data structure, you have got to read it up and get your hands dirty and implement it yourself. There is no way around this.
This is a bit like taking notes in classes. The notes themselves are (nowadays mostly) almost worthless, with easy access to textbooks and other resources. The fact of taking the notes is what actually counts.
I am surprised so many talented engineers went the touchscreen route. Volkswagen, Mercedes and more recently BMW are going this way. In my experience it is not only annoying, it is a safety hazard. In my old car, I could feel for the button to turn on the defrosting without ever taking my eyes off the road, it was so well designed!
In a way, it feels that the current trend is very much like the Apple laptops at some point, where they god rid of the physical function keys and replaced them with touch sensitive controls. Thankfully, Apple is reverting this change.
I think at some point car manufacturers will realise that it leads to more accidents and they will also reverse course. Perhaps touchscreens will even be forbidden?
Caveat: I was wrong before on touchscreens. I though phones with touchscreens will not work out, but they have. However, it is because we no longer use phones for phoning, but to watch movies, read text, etc.
I have an anecdote to offer: in the early 2000s I was learning to drive in a former comunist country. Most cars were Dacia 1310, a copy of 1970s Renaults. The stick was awful, the steering was very heavy (as in lifting weights heavy), the clutch was terrible. It was very difficult to drive one, let alone learn to drive one. Newer and better cars were just beginning to appear, but there were few of these and they were expensive. There were two lines of thought in my circle: (1) that you should learn on a Dacia, because then you will be able to drive anything and (2) you should learn on a modern car, because it is easier. Needless to say, camp (2) won: the Dacias all but disappeared and furthermore, newer cars are mostly automatic.
So I wouldn't hold my breath that the manual gear shift will survive.
When a field is young, it is simpler to make important discoveries, so in that sense, science is (obviously) getting harder.
But most of the graphs can be explained by the sheer number of papers being published.
Academics have the perverse incentive to publish as many papers as possible, instead of discovering as many interesting things as possible, because items published is way easier to measure than real progress made.
Therefore there is a significant paper inflation problem. People might today write 10 papers with LPUs (least publishable unit) with stuff that would have been a single technical report 30 years back.
This is much worse than it sounds, because it affects productivity significantly in subtle ways: it takes effort to publish those 10 papers, it takes effort to read up and review the 10x papers of others, and it takes time to think about LPUs instead of concentrating on the bigger picture.
Unfortunately, due to the way the research system is set up, it is not likely things will improve.
While losing weight, I would not replace it, but simply remove it altogether. Bread is not an essential nutrient (although obviously French baguettes are great tasting). You can get plenty of carbs from other food (e.g., fresh fruit).
The key here is "it looks like they are equivalent".
In fact, I am not sure they are equivalent (in general, without taking into account the context), and even if they were, proving this would be S.F. for a compiler today (2020). Even coming up with such an optimisation without hardcoding it does not seem plausible.
That looks interesting. The code is not simpler to understand nor is it more efficient, but it seems to work, assuming target is in the list. How would you represent the empty list?