I've recently taken a course on Logic and Computability where I studied first-order logic. However I recall using throughout my career in computer science, different expressions of first order logic that differ from the one in textbooks. This is especially noticed when quantifying over different "types". For example:
"For every natural number $n$, there is a computable of code $n$" could be written as: $$\forall n: \mathbb{N} (\exists p: \text{program (code}(p)=n)$$
This isn't technically a first-order formula, because it doesn't follow the rules of the first order language: one cannot specify the type of the quantifier. However on many occasions, I find this type of notation, but I can't manage to figure out how a translation to the 'classic' first order would be. I can't omit the types and have the universe of the interpretation be the union of natural numbers and programs, because this would mean that when quantifying I'd have to do it over both. And also, functions and predicates would have to be defined over the union. Any ideas?