Tarski's Convention T is not strictly speaking a definition principle for truth - it is an evaluation condition on whether a given axiomatically theorised predicate is a "Materially Adequate" definition to count as a Truth predicate.
The work that Tarski did in showing how a truth predicate could be defined was not in presenting the T-Schema. That "snow is white" ought to be true if and only if snow is white is just something that Tarski reckoned anything that might be called "Truth" ought to satisfy, in the same kind of common-sense way that might meet your children's exacting standards.
Tarski's work was presenting a way in which we might take our formulae of first order logic and understand what mathematical sense we might make of them. Tarski started by presenting the idea of a Model, as being an algebraic characterisation of a domain of objects, relations over and between those objects, for a class of names, constants and relation/property terms in our logical language, and a notion of an interpretation function that connects the various terms in our language to either objects or relations in our model.
A model deems an atomic sentence P(a) (or is_White(snow)) true (or sometimes we say "value 1" to distinguish it from the question of the Truth predicate) if the interpretation of a is an object in the domain that is a member of the relation interpreted by P (that snow, being the interpretation of snow, is a member of the set of white things, being the interpretation of the predicate is_White(x)).
Then, the interesting aspect of Tarski's notion of a model is it matches the compositional structure of logical language, so we can add connectives like "and", "or", and quantifications like "every", "some" as part of how we mathematically model the domain of objects we're interested in, and build up more complex sentences from the basic cases. So thanks to using the maths of model theory, we can make sense of something Not being white, of what it would mean for everything to be white, or (given that there are other colours) how we might test whether something is "white and not some other colour" etc.
By making mathematical sense of a logic in a model, Tarski showed that we could in principle define a Truth predicate over an interpreted language as a way of considering well-formed value 1 logical sentences as a class of "True sentences". He did this through a notion of what it takes for an object to satisfy an open formula. This is interesting, because it shows that there is not only a sensible and useful algebra for logical languages, but also a sensible and useful algebra for modelling logics and reasoning about how evaluated sentences might relate to one another. So if we want to be able to comparatively evaluate different logics or theories, we can use a Tarski-style definition to build mathematical models of their sentences and use mathematical tools to analyze them. As an example of how you might use this definition, suppose we might ask a sequence of logical questions, and want to test whether the resulting answers are all true. If Truth is well defined, there exists in principle a way of testing all of our sentences to show that they are all members of that class.
Fortunately, for standard models, Tarski's construction satisfies the principle of the T-schema - a given sentence is a member of the class of True sentences just in case the sentence interpreted in the base model is given the value 1 through the model-theoretic semantics. So there is a fairly simple algorithm for evaluating all of some set of sentences for truth - namely, interpret them in the base model and evaluate them, continuing on if they get value 1 and returning if any gets value 0. This isn't going to be true of all sentences in all models (consider - the Liar sentence "this sentence is not true"), but the construction shows how we can characterise a truth predicate over some base model and thus treat it as itself an object for comparative evaluation.
You can have a look at the SEP Article on Tarski's definitions for a more worked-through explanation of the mathematical project he was trying to build. A concrete instance of how this kind of reasoning sheds light on practical problems in mathematical logic is in the idea of reducing quantified logical sentences to a Skolem Normal Form, which massively simplifies the problem of automated theorem proving. We can do this because Skolemized sentences are "equisatisfiable" with their quantified counterparts.
What we might say is that software specification and verification ought to be suitably founded in a semantics in just the same way that first order logic is founded in the model-theoretic programme following on from Tarski's initial discoveries. In formal computer science, this is studied in the field of Denotational Semantics and other related programmes, and some of the ideas about what kind of axiomatizations there are for correct software (and also hardware) behaviour are considered in Formal Specification and Verification logics such as Floyd-Hoare logic.
