technically, „formal verification” could be meant to be verifying just a property as pointless as „the program never tries to open „…/fuck_this_shit.txt”” (which would be simple if the code contains a check before every open() call), but in real field, formal verification extends to devizing a clear concept, and proving a state-of-the-art set of properties (modulo some unproven hypotheses, like „RSA is secure”).
by definition, if the software satisfies all that is asked of it, it can no longer be called buggy, especially if the specification includes all state-of-the-art properties:
- the software doesn’t crash.
- every call to the software eventually returns. or even: the response time is bounded.
- the operation of the software is consistent with a simple model.
plus, the „implementational” layer of the software usually goes through a rigorization filter (eg. the above properties for each function). at this point, all run-time bugs of the classical kind have been eliminated.
- the operation of the software is also consistent with other simple models.
- the software fulfills a set of additional goals (including the absense of other kinds of faults).
at this point, if the specification is precise (ie., no points like „the software works PERFECT™ly”), one can be damn sure that there is no oversight in the specification, ie. maybe this software is not captured by the „all software is buggy” clause. depending on the application, the set of goals may include eg.:
- the software is secure (eg. with respect to an actor/operator model).
- the data transformation performed by the software is invertible (lossless compression).
otherwise, nothing else can come as close to software perfection than clean design, redundant analysis of the specification, coupled with formal verification of the implementation.
what is state-of-the-art may get broader in the future. for example, there ought to be a property like „there is an evident absence of backdoors.”, but the practice of formalizing such properties is yet to come, but one step in this direction is:
- the software only makes calls to the system if necessary; at the very least, the set of system functions ever used is very limited.
- teleporting through danger (eg. instakill) zones, and warping to be harder to hit, via laghacks (technically in the game module).
plus, for reference, i can name some bugs of the past, like:
btw, i should also note that the game module is also hardly sandboxed on the server, but it should be — any client should be able to upload gamelogic code, and have it run after appropiate voting, and it should be easy for the then-current clients to restore fail-safe gamelogic code on the server.
because this is crappy design. it is crappy because it is not consistent with the expectation from general users, and it is possible to do much better in this regard.
- non-encryption effectively strips users of the reasonable possibility to enforce their right to privacy.
- non-authentication opens a hole for user impersonations (regular, or even admin) and stealing/destruction of private or otherwise important data.
eg. the client has to decide whether „models/wtf/a_tweeping_boop.md3”, combined with a random shader, looks like a human. how easy is this ?