[peteroh]

1. This "unsoundness" was the subject of extensive (endless) discussions on the Infer team (as you can imagine). This spurred some theory and there are some precise theorems associated with how parts of Infer work. E.g., racerd has some theorems and over a period of a year saw no observed false negatives, so I'm not sure it's accurate to say that it's "just an ordinary unsound static analysis" (see https://dl.acm.org/doi/10.1145/3290370 and references).

2. Apart from that, to me, if logic inspires (part of) the design of an analyzer, that's perhaps more valuable than using logic to judge it after the fact, as analysis design is hard; and this is true even if analyzer ends up following part of the spirit if not the letter of the logic.

I believe I get where you care coming from, though, and appreciate your perspective. :)

[haskellandchill]

Oh wow, this thread has attracted some notable participants. Much respect for your work. While you're here I've been wondering about applying all this stuff to the problem of having an unknown computing environment and bootstrapping a sane workspace on top of it. That might not make sense. I'm at a loss for how to explore the literature. Something like ubiquitous/pervasive computing with service discovery combined with foundational proof carrying code, certified compilers, verified stacks, etc.