Abstract: Mobile computing is a new computing paradigm based on networking. This paper aims to reveal the essence of mobile computing from the point of view of formal abstraction. At first, four features of network computing are analyzed and outlined, inducing five programming principles for mobile computing. Then several representative formal models and methods concerning mobility are introduced, which include formal calculi based on process algebra such as π calculus, ambient calculus and Seal calculus, distributed temporal logic such as mobile Unity, and extended Actor model. In addition, some critical notions and properties of mobile computing such as location, mobility, interaction, dynamic reconfigurability, and resource control are analyzed and discussed for each formalisms. Finally, comprehensive analysis and comparison for these formalisms are carried out. All of the results can help to make a substantial foundation on the research of formalisms for mobile computing.