Programming and debugging wireless sensor networks is a hard task, not only due to the fragility and volatile nature of the hardware, but also, on a very fundamental level, due to deficiencies in the current programming tools. In this paper we propose a distinct approach to the design and implementation of programming languages for wireless sensor networks. We argue that such languages should be type-safe as this allows an appropriate compiler to prematurely (statically) detect programs that otherwise would produce run-time errors. Moreover, we argue that the specifications for the language run-times should be proved to preserve the language semantics, thus removing a semantic gap that can be observed in current systems. We present a type-safe core programming language for sensor networks called Callas and provide a specification for a virtual machine for it. We prove that the virtual machine preserves the programming language semantics. This establishes Callas as a robust semantic framework for designing and implementing higher level programming languages for wireless sensor networks.