Typically, philosophers would not consider a belief about a formal system justified unless that belief is backed by a proof. In software, for known behavioral

Typically, philosophers would not consider a belief about a formal system justified unless that belief is backed by a proof. In software, for known behavioral specs, you don't have a real justification until you write a formal proof. Just because formal proofs are uneconomical doesn't mean there's some fundamental philosophical barrier preventing you from verifying your UI code. Doing so is not just possible, there are even tools for doing it. So really, this is not a Gettier case, because in formal systems a true justification is possible to construct in the form of a mathematical proof. An example of a Gettier case in a software system would be formally verifying something with respect to a model/spec that is a Gettierian correct-but-incorrect model of the actual system. There are almost no software systems where we have true JTB (proofs), so there are almost none where Gettier cases really apply. Uncertainty in software is more about the economics of QA than it is about epistemology or Gettier style problems, and that will remain true until we start writing proofs about all our code, which will probably never happen.