Theoretical computer science has offered various computation models like automata, Turing machine, lambda calculus, and their importance to theoretical work and to practice is widely recognized. The progress of the classical topics of formal language theory, computational complexity, and mathematical semantics of programming languages is due to these computation models. In this talk we propose two challenges that have tight connection to mathematical theory of programs and probably need new computation models to attack them.