The model theory of programming languages is called denotational semantics. You can google the term to find out more about it, I'll give an extreme synthesis of it.
Denotational semantics is a special case of "categorical logic", which is itself a generalization (introduced in the 1960s by Bill Lawvere) of the usual model theory of first-order logic. The idea is that a programming language may be seen as a (syntactic) category whose objects are combinations of basic types (Booleans, natural numbers, etc.) and whose arrows are equivalence classes of programs depending on a finite number of arguments. When I say "combinations of basic types" I mean that usually the syntactic category has at least products and a terminal object, the rest depends on the language. I am not going to explain what it means for two programs to be "equivalent" (and therefore to represent the same arrow in the syntactic category), but intuitively it means that they "evaluate to the same thing".
For example, for your program $f$, if the multiplication you use in its definition has type $A\times A\to A$, then $f$ would be an arrow of the syntactic category of type $A\times A\times\mathsf{nat}\to A$. (Programs that do not return anything are typed with the terminal object).
Now, depending on your programming language, its syntactic category $\mathcal C$ will have a certain structure and properties (like I said, it will have at least finite products). Then, your language will have (denotational) models in any category with that structure and properties. Given such a category $\mathbf D$, a model is just a structure-and-property-preserving functor $F:\mathcal C\to\mathbf D$. For example, $\mathbf D$ could be $\mathbf{Set}$, so your types will be interpreted by sets and your programs by functions. More often, $\mathbf D$ will be a category with the property that every arrow has a (least) fixpoint, because fixpoints are needed to interpret recursion. A famous example is $\mathbf{Cpo}$, the category of complete partial orders and Scott-continuous maps.
The fact that the category $\mathcal C$ is "syntactic" means, a bit more technically, that it is sort of the "free category" with such and such structure/properties built from the syntax of the programming language. Therefore, the functor $F$ corresponding to the denotational model will be defined as soon as you define it on the basic types and on the basic pieces of the syntax of your programming language. This is precisely what happens in the usual model theory for first-order logic, where a model is defined as soon as you fix a set (more generally, an object of a category) interpreting the universe where your individuals live, and a function/relation (more generally, a morphism/subobject) for every function/relation symbol of your logical language. The fact that the model must verify the axioms of the theory correponds, in denotational semantics, to the fact that the arrows of the syntactic category are equivalence classes of programs, so your denotational model must equate equivalent programs.
A final word of warning: in many expository texts on programming languages, denotational semantics is presented directly as an interpretation of the basic pieces of syntax into a certain category, without any reference to the functorial perspective or the construction of the syntactic category, so don't be surprised if you do not see that appearing explicitly.
Addendum: let me clarify how categorical logic is able unify traditional model theory (of first-order logic) and denotational semantics.
The categorical viewpoint on traditional model theory is that every first-order theory $\mathbb T$ induces a Boolean pretopos $\mathrm{Syn}(\mathbb T)$, the syntactic category of $\mathbb T$. It doesn't matter what a Boolean pretopos is exactly, all it matters for the sake of this answer is that the category $\mathbf{Set}$ of sets and functions is a Boolean pretopos, and that we may define a (very large) category of Boolean pretoposes and morphisms between them, which are functors preserving all the properties that make a category into a pretopos.
One of the pillars of categorical logic (the observation originally due to Lawvere) is that a model of $\mathbb T$ in the traditional sense is exactly the same thing as a morphism of Boolean pretoposes
$$\mathrm{Syn}(\mathbb T)\to\mathbf{Set}.$$
As I said in the comments, one may take another Boolean pretopos as $\mathbf{Set}$, and get models in that pretopos. For example, if $\mathbf{FinSet}$ is the category of finite sets, then a morphism $\mathrm{Syn}(\mathbb T)\to\mathbf{FinSet}$ is a finite model of $\mathbb T$.
As Andrej pointed out, the theory of programming languages is more similar to universal algebra at this level, in the sense that a programming language may be seen as an equational theory: there are no logical operators, quantifiers, or anything like that, only terms (representing programs), built out of function symbols (or "term-formers"), and equalities between them (representing the so-called "operational semantics" of the programming language). Also, with respect to first-order logic, there are types, that is, the equational theory is multisorted (in traditional model theory, every first-order theory implicitly has only one sort).
However, the idea of (denotational) model is exactly the same as that of first-order model. For example, the theory $\mathbb G$ of groups is a (single-sorted) equational theory, and a group in the traditional sense is just a product-preserving functor
$$\mathrm{Syn}(\mathbb G)\to\mathbf{Set}.$$
Here, changing the target category is very useful, and you have even more freedom than in (classical) first-order logic because you have less properties to preserve (equational logic is much simpler than first-order logic--in fact, in this case all you need is a category with finite products, which is way less than a (Boolean) pretopos). For example, product-preserving functors $\mathrm{Syn}(\mathbb G)\to\mathbf{Top}$ are topological groups, product-preserving functors $\mathrm{Syn}(\mathbb G)\to\mathbf{Sch}$ are algebraic groups, etc., all objects which naturally come up in mathematics. Categorical logic gives a uniform account of all this variety of structures.
Similarly, when one defines a denotational model of a programming language $\mathbb P$ in which types and programs are interpreted as objects and arrows of some category $\mathbf D$, one is implicitly defining the syntactic category $\mathrm{Syn}(\mathbb P)$ and a structure/property-preserving functor
$$\mathrm{Syn}(\mathbb P)\to\mathbf{D}.$$
The big difference with model theory, pointed out by Martin Berger in his comment, is that, in the theory of programming languages, there is no canonical class of categories, fixed once and for all, such that $\mathbf{D}$ and $\mathrm{Syn}(\mathbb P)$ belong to that class. This is in sharp contrast with first-order logic (where we have (Boolean) pretoposes) or algebraic theories like $\mathbb G$ (where we have finite-product categories). In other words, there is no canonical "logical structure" that we know $\mathbb P$ must have (unlike first-order theories or algebraic theories): it all depends very much on the kind of programming language that $\mathbb P$ is. This is ultimately due to the lack of a formal definition of "programming language".
That being said, there are some important cases, encompassing many useful situations. For example, a typical categorical structure for programming languages is that of a Cartesian closed category with a natural number object and a fixpoint operator, which is enough to define a Turing-complete programming language. (This shows, in particular, that you cannot take $\mathbf D=\mathbf{Set}$, because $\mathbf{Set}$ does not have a fixpoint operator. So being able to vary the target of the intepretation functor is a generalization which is absolutely fundamental to programming languages!).
Another big difference with traditional model theory is that, usually, people do not study the relationship between various models $F:\mathrm{Syn}(\mathbb P)\to\mathbf D$ for a fixed $\mathbf D$, because they differ in uninteresting ways. For example, when $\mathbb P$ is the simply-typed $\lambda$-calculus, the only choice you have in defining $F$ is to pick an object of $\mathbf D$ for each atomic type, and the specific choice is often irrelevant. So, contrarily to first-order logic, it is interesting to change $\mathbf D$ rather than pick a $\mathbf D$ and then let $F$ vary. In fact, when people say that they have a "model" of a programming language, usually they mean that they have a $\mathbf D$ with the desired structure/properties, not that they have fixed one specific $F$. This is another reason why denotational semantics has a different flavor than usual model theory, even though technically they are related via categorical logic.
By the way, all this (long!) digression was only to drive my point home: denotational semantics is to programming languages what model theory is to first-order theories (with all the necessary caveats). You do not need to know categorical logic in order to understand or study denotational semantics!
