Explore type-driven program synthesis and its applications in improving software quality through this conference talk. Delve into the use of declarative constructs and program synthesis technology to translate specifications into executable code. Learn about refinement type checking as a verification mechanism that combines types and SMT solving for automatic reasoning. Discover two applications: Synquid, a tool for creating recursive functional programs from refinement types, and Lifty, a language that uses type-driven synthesis to repair information flow leaks. Examine case studies involving complex data structures, information flow policies, and automated access check insertion. Gain insights into the future of programming, including orthogonal concerns, information security, and resource-aware programming through synthesis-aided techniques.