My research sets out to show that we can design computers that are guaranteed to interact correctly with the physical world. The solution to this challenge is the key to enabling computer assistance that we can bet our lives on. My research pursues this challenge with the principled design of programming languages with logic that can provide proofs as correctness guarantees. Whether in cars, aircraft, or robots, the decisions that their computer programs reach have a crucial impact on all of us and they have the potential to make the world a better place. Computer programs can help us drive cars, help pilots fly aircraft, and enable robots to help the humans that they are interacting with. Along with these exciting prospects comes the responsibility to get the programs correct, though, which is quite a difficult challenge in light of the vagaries and uncertainties of the physical world.