We will present Quantum Predicative Programming - a theory of developing programs intended for execution on a quantum computer. It is the most general theory of quantum programming proposed today. Our formal framework provides a methodology to rigorously specify, implement, and analyse quantum algorithms, the paradigm of quantum non-locality, quantum pseudo-telepathy games, computing with mixed states, quantum communication protocols, and quantum cryptographic protocols. Our work takes a step beyond what formal verification traditionally addresses, namely proofs of correctness. The framework provides tools to formally express and verify such properties of quantum systems, quantum algorithms and quantum protocols, as time, space, and communication complexity.