The thing that I find troubling -- in spite of following and enjoying the progress in program verification -- is that in every other scientific-professional discipline, like medicine, researchers always caution about misrepresenting results (this drug looks promising, it works on mice, and it may hold promise for humans; they get annoyed when the media is overly optimistic) and virtually all practitioners are even more skeptical than the researchers. In CS/software, people make some progress in verifying a specific property of a specific lab-sized program, and many practitioners declare "halting problem solved!" (I'm exaggerating, but that's the gist). I get the feeling that a few researchers tacitly encourage this state of affairs. I see this in PLT more than in any other subdiscipline of CS (along with -- maybe -- machine-learning).
There is constant progress on many fronts, and it's perfectly OK to get excited, but hyped overpromising has led to significant setbacks in CS in the past (including in formal methods in particular) because the greater the hype the greater the disappointment. We should be happy with what we have without claiming (falsely) that all of our problems are solved. If anything, cautiously downplaying research results is a much better strategy to long-term success.
I think there are different discussion forums for different things. Right here, I'm talking to you because I'm interested in hearing your point of view and perspective, and I want to know how you react to mine.
In a professional context it is expected to downplay results and to be very cautious. Research is an expensive and volatile investment at the best of times, and overstating your success to secure funding could easily lead us into the next AI winter... So if we were to meet at a conference, I would still hold the same views, but I would never express them in a talk or in any other official capacity.
If you see researchers overpromising results, e.g., in the contributions section of a paper, then that is very bad form.
I think healthy skepticism is no less important in professional settings than in academic settings. I don't think pharmaceutical researchers oversell research drugs to physicians (although drug salesmen certainly do), and if they do, it's just as bad, and I hope doctors are skeptical.
The thing that I find troubling -- in spite of following and enjoying the progress in program verification -- is that in every other scientific-professional discipline, like medicine, researchers always caution about misrepresenting results (this drug looks promising, it works on mice, and it may hold promise for humans; they get annoyed when the media is overly optimistic) and virtually all practitioners are even more skeptical than the researchers. In CS/software, people make some progress in verifying a specific property of a specific lab-sized program, and many practitioners declare "halting problem solved!" (I'm exaggerating, but that's the gist). I get the feeling that a few researchers tacitly encourage this state of affairs. I see this in PLT more than in any other subdiscipline of CS (along with -- maybe -- machine-learning).
There is constant progress on many fronts, and it's perfectly OK to get excited, but hyped overpromising has led to significant setbacks in CS in the past (including in formal methods in particular) because the greater the hype the greater the disappointment. We should be happy with what we have without claiming (falsely) that all of our problems are solved. If anything, cautiously downplaying research results is a much better strategy to long-term success.