From the logician's point of view among problems of quantum physics there are two key ones: the lack of geometric interpretation of essentially syntactic operator formalism and the lack of satisfactory mathematical definition of the notion of limit used in physical practice. We address these problems and propose a (hyper-finite) model of quantum mechanics in which both issues have been resolved. As an application we present rigorous calculations of Feynman propagator for particles with quadratic potential, both directly and via path-integration. We then discuss the possibility of extending the calculations to particles with arbitrary potential.