OO, actually, is a big part of a problem. OO is inherently stateful, so reasoning about OO programs is just slightly easier than reasoning about assembler prog

OO, actually, is a big part of a problem. OO is inherently stateful, so reasoning about OO programs is just slightly easier than reasoning about assembler programs. OO was introduced as a way to control program behaviour - encapsulate effects, hide information about effects, abstract effects away. All while controlling them. Using single notion of object and inheritance, as a single method of type derivation (ie, derivation of information to reason about). This is hardly done now, with all the power of Coq type system, why should be it possible within typical OO type system of mid-90 or even current .Net type system?