Software is integral to the fabric of our lives, controlling transport, the economy and infrastructure, and providing the main tools of work and leisure. The cost of software failures is therefore high, to productivity, stability, safety, and privacy. As an indication of the economic impact, it is estimated that software errors cost the US economy tens of billions of dollars last decade. Software errors can also impact human safety as software is used to control transport, infrastructure, and medical equipment. The research agenda of program verification aims to mitigate these risks by putting software engineering on a rigorous foundation through techniques to guarantee program correctness. As software becomes more complex and pervasive, program verification is ever more important. This work aims to advance the state-of-the-art in verification at the point of program development through advancements in programming language theory and practice. Programming languages are the core tool in which software is constructed; they are the means of communicating our intentions to computer hardware. There are various design trade-offs when creating a programming language, which has led to the variety of programming languages in use today. Some languages support verification by including a "type system" which categorises data and operations, ensuring that operations are only applied to data of the correct type. This provides some guarantees about the correctness of the program by ruling out various kinds of error before the program is ever executed. A subfield of programming language research aims to make type systems more expressive so that they can describe and enforce more properties of programs and thus raise the level of verification possible within the language. The current proposal aims to do just this, focussing on the notion of data as a "resource" subject to constraints which should be enforced by a language's type system. This project develops a particular technique for building such type systems in a way that can capture various kinds of property in one system. The manipulation of data is central to the task of programming. Current programming languages essentially view data as an infinitely-replicable resource that can be stored, manipulated, and communicated without restriction. However, this perspective is naive. Some data is private and thus should not be arbitrarily copied, stored, or communicated. Some data is large and thus should not be replicated too frequently. Some data acts as a way of interfacing with other parts of a system, e.g., files or communication channels, which are then subject to restrictions on how they can be used, such as agreed protocols of interaction. Most programming languages are agnostic to these constraints however, treating data as totally unconstrained. This can lead to various software errors, including privacy breaches, performance problems, and crashes due to incorrect interactions between parts of a system. The goal of this research is to embed the constraints associated with data into the type system of a language so that these additional constraints can be automatically enforced. The key technology for doing this is a novel notion of types called "graded modal types" which can capture and track different kinds of information about the structure of programs and the flow of data through them. This work will develop the theory and practice of graded modal types, producing a prototype language that demonstrates their use for verifying program properties. Three case studies will be carried out to demonstrate their power: (1) ensuring privacy and confidentiality, (2) capturing and reasoning about performance e.g., how fast a program will execute relative to the size of its inputs and how much memory it will consume (3) enforcing fine-grained protocols of interaction. This work is a step towards a new generation of trustworthy software.