As is widely accepted, modern C++ is difficult for beginner engineers, especially for its features in generic programming. I am also an engineer using C++ in industry. I felt it difficult to understand documents here and there. Luckily, I understand FOL and set theory at a certain level and I believe it is elegant and useful to organize features in a language or across languages using some formal system. Unfortunately, I don't understand lambda calculus in detail. As an engineer with traditional math background, I learned FOL from understanding ZFC set theory and this is why I have been using FOL to explain C++, rather than a system from TCS. In fact, I can use FOL to explain C++ to some degree, but I am not sure if FOL is so powerful as to explain all features of generic programming in C++.
For example, here is a simple c++ template declaration:
template <typename T>
class MyClass
{
private:
T mem_var;
public:
template <typename S>
T func(const S& var)
{
return some_operation(mem_var, var); // assume that some_operation returns T
}
};
It is my understanding that we get two statements after declaring this class template. First, for each class (set) $T$, there uniquely exists some class $x$ whose name is MyClass and for any $y \in x$, there is some variable $z$ whose name is mem_var and $z$ is a member of $y$. With this statement, we can introduce a function symbol MyClass (and a new first-order system) such that each MyClass(T) is a solid symbol. Second, for each class $T$, for each class $S$, there exists a unique function $f$ whose name is func and for any $x \in $ MyClass(T), for any $y \in S$, $P([f(x)](y))$, where $P$ is a predicate that indicates the result of an action $f$ conducted by a subject $x$ using data $y$ (note the philosophy of object-oriented programming indicated here).
Is FOL adequate for interpreting all features of generic programming in C++? In fact, I am also assuming that state machine has to be used to update the system so that status update of objects may be considered.