Unifying sets and programs via dependent types

We present a foundational framework, which we call D, unifying a lazy programming language with an impredicative constructive set theory IZFR by means of dependent types. We show that unification brings many benefits to both worlds. First, D supports two paramount paradigms of creating reliable software: correctness by construction and post-construction verification, while retaining the expressiveness of set theory. Second, D provides new expressive power, which makes it possible to internalize and prove inside D the standard meta-theoretic properties of constructive systems, such as Numerical Existence Property and Program Extraction. Finally, computation arising from the programming language significantly enriches set theory, as we show that D is stronger than IZFR and that its real numbers behave in a better way.