I was merely reiterating a common (and I think sensible) point that we can't write proofs about things we don't have the computational resources to address or just plain don't realize are an issue. Both are very real challenges to using proofs about our software, and should be kept in mind when talking about the field.
The said, Im a proponent of everything from proofs about abstract algorithm properties to basic model checking on a spec to using formal methods to extract a program with guaranteed propertied from a formal spec we've written proofs about in something like Coq.
DARPA funding HoTT research should clue anyone in that this stuff is useful.
I just see people talking about domains and saying, "We don't need proofs for software" like they learned literally nothing from OpenSSL last year. And perhaps they did not, but I think we all should recognize that the stakes are getting pretty high and it's time to stop pretending we're all supervillan-level software designers.
You're right that you can take a mathematical proof out of the realm of abstract math and it's new domain may not have all the guarantees we need, but this means we need to extend the system to account for the new domain (and within this domain, the proof is not valid).
But the poster doubled down on this idea that "there are constraints proofs ignore" within the existing domain. Outside of convenient proofs that upper division students provide, this is not true.
A good example of this process and the nature of "pure" CS interacting with the real world is the field of distributed databases. As the field has grown, proofs are expected to aggressively model real world conditions and in fact go further, modeling outright adversarial conditions unlikely to occur in the real world.