Wireless sensor networks are notoriously difficult to program and debug. This fact not only stems from the nature of the hardware, but also from the current approaches for developing programming languages that targets these platforms. In particular, current systems do not place enough stress on providing formal descriptions of the language and its run-time system, and on proving important static properties. As a contrasting approach, we design, implement, and deploy a programming language along with a run-time system that enable us to prove two fundamental static properties: the type-safety of the language and the soundness of its run-time system. These properties ensure the absense of an important class of run-time errors in sensor network applications, which shortens development time and simplifies debugging.