 Each of the different approaches on software verification examined in the previous section assumes a different understanding of correctness for software. Standardly, correctness has been understood as a relation holding between an abstraction and its implementation, such that it holds if the latter fulfills the properties formulated by the former. Once computational systems are described as having a layered ontology, correctness needs to be reformulated as the relation that any structural level entertains with respect to its functional level (Primiero, 2020). Hence, correctness can still be considered as a mathematical relationship when formulated between abstract and functional level; while it can be considered as an empirical relationship when formulated between the functional and the implementation levels. One of the earlier debates in the philosophy of computer science (De Millo et al. 1979; Fetzer 1988) was indeed around this distinction.