CoRecursive: Coding Stories
Episode: Refinement Types and Liquid Haskell With Niki Vazou
Host: Adam Gordon Bell
Guest: Niki Vazou, Assistant Professor at IMDA Software Institute and Creator of Liquid Haskell
Date: May 15, 2019
Episode Overview
This episode delves into the world of refinement types, formal verification, and the journey toward making theorem proving a mainstream part of programming. Adam Gordon Bell interviews Niki Vazou, a key contributor to Liquid Haskell, discussing how refinement types can push software verification forward, what sets them apart from dependent types, the use of SMT solvers, and the challenges and opportunities for bringing advanced type systems to everyday programming in mainstream languages.
Key Discussion Points & Insights
The Vision: Bringing Theorem Proving to Mainstream Programming
- Niki’s goal: Make formal verification usable for mainstream programmers—not just experts.
- “Some developer is going to write code and then some verification will run on the bug that will not only detect errors, but also ... suggest code or to make coding easier, faster and safer. But ... the developers should not know exactly what is going on in the background.” – Niki (01:42)
- Importance of reducing the “fear factor” around advanced verification tools among everyday developers.
What are Formal Verification, Types, and Refinement Types?
-
Formal Verification:
- Ensures code complies with specifications written in a formal language.
- "The high-level idea is that you have a code, you have some specifications ... then you find a way, like refinement types, to express these specifications formally ... and then formal verification is the process of trying to prove that the code satisfies the specifications." – Niki (02:36)
-
Types as Verification:
- Types group programs/expressions into sets, allowing guarantees about allowed operations (e.g., integer function only accepts integers).
-
Refinement Types:
- Extend standard types with logical predicates.
- Example: Instead of
Int, specify that an integer is non-zero for a divisor function:- “You can refine the standard types ... with logical predicates ... like V is different than zero. And you give this refinement to the second argument of the divisor operator...” – Niki (06:57)
How Refinement Types Compare to Dynamic Checks & Performance
-
Compile-time vs. Runtime Checks:
- Traditional approach: use runtime checks or sentinel values (e.g.,
None). - Refinement types move verification to compile time, improving efficiency:
- “What refinement types do is basically at compile time trying to prove that this check always succeeds. So they basically make your program more efficient, faster...” – Niki (08:06)
- Traditional approach: use runtime checks or sentinel values (e.g.,
-
Examples:
- Avoid division by zero and out-of-bounds memory access by encoding constraints in the type system.
SMT Solvers: The Backbone of Refinement Type Checking
-
Role of SMT Solvers:
- SMT = Satisfiability Modulo Theories.
- Used as black boxes to answer whether logical predicates about programs are universally true.
- “Me as a researcher ... I want to build formal verification and type systems that the user will use without ... knowing what happens here.” – Niki (11:11)
-
Analogy to Sudoku:
-
Interaction with Type Inference:
- The refinement type system translates code + specification into SMT queries; if the SMT cannot confirm the property everywhere, it results in a refinement type error (14:57).
Propagation of Constraints & Working with Real-World Data
-
Handling User Input:
- Input from the outside world needs runtime checks, but once checked, refinement types enforce constraints throughout the call graph.
- “Instead of having this runtime check ... at the end division operator, then I have much fewer runtime checks at the beginning of my code where I take the input from the user for which I know nothing.” – Niki (16:08)
-
Type Error Reporting and Runtime Checks:
- Refinement type errors suggest (but do not explicitly direct) where runtime checks are needed (18:08).
Refinement Types vs. Dependent Types
- Refinement: restricts existing type systems; rejects more programs.
- Dependent Types: expand the expressiveness; accept more programs.
- “So dependent types make extend the type system to accept more programs, while refinement types constrain the type system so that more programs are rejected.” – Niki (19:47)
- Proof Construction:
- Dependent types require manual proofs or tactics in-code.
- Refinement types rely on external solvers for (often automated) proofs (19:47).
Real-world Implementation: Liquid Haskell & Other Languages
-
Liquid Haskell:
-
Other Language Support:
- Started in OCaml, also explored for Ruby and JavaScript.
- Noted practical and cultural challenges when bringing refinement types to dynamic or less type-oriented languages (23:33, 28:58).
- "It is a thing that languages like Haskell adapt 20 features, maybe in five years, like two of these features will become mainstream and will be ported to JavaScript..." – Niki (24:11)
- Scala example: Uses macros and a more intertwined relationship with the type system (25:57, 26:08).
Motivation, Usability, and Error Reporting
-
Mainstream Adoption:
- Niki emphasizes refinement types’ potential for making advanced verification approachable for average programmers.
- Error reporting and automation are key usability challenges (30:43).
- “...error reporting is the process of trying to explain to a human why the algorithm failed. And the more difficult the algorithm is, the more messy the error message is...” – Niki (30:43)
-
Future Potential:
- Suggestion: Compilers could someday utilize refinement information to optimize code and resource use (32:12).
Proofs as Programs & Liquid Haskell for Theorem Proving
-
Proving Laws as Code:
-
Educational Tool:
- Liquid Haskell is recommended as approachable for learning formal proofs, especially for Haskell programmers (36:54).
- “Especially if you know Haskell, then it's very easy to learn using liquid Haskell, how to express formal reasoning and proving formal properties about your Haskell program.” – Niki (37:02)
-
Caveats:
Working with Compiler Internals
- Leveraging GHC:
Verification Tools Beyond Academia
-
Adoption in Industry:
-
Distinguishing from Tests:
- Verification proves properties for all cases, while tests check behavior against particular examples (48:46).
Memorable Quotes & Moments
- “My goal is to make theorem proving a useful part of mainstream programming.” – Niki (01:24)
- “What is important is that the developers should not know exactly what is going on in the background. Because ... especially mainstream developers, are all these scared of this formal verification ...” – Niki (01:42)
- “Types give us some limited form of verification.” – Adam (04:42)
- “Refinement types basically take the standard types and refine them with some logical predicates ...” – Niki (05:42)
- “The standard example is division by zero ... you can go and insert logic to this type and say, give me an integer, then give me an integer that is probably different than zero.” – Niki (05:42)
- “Refinement types are awesome, specifically when your program is correct.” – Niki (29:29)
- “Error reporting is the process of trying to explain to a human why the algorithm failed. And the more difficult the algorithm is, the more messy the error message.” – Niki (30:43)
- “... you will spend a lot of time writing tests anyways, right? ... our goal for I guess the more academics is to make it be a small step from the tests to actual verification.” – Niki (47:42)
- “A test only ... can only check for the absence of a problem, right? ... what you're talking about is verifying like for all inputs.” – Adam (48:46)
Timestamps for Key Segments
| Timestamp | Segment / Theme | |-----------|------------------------------------------------------------| | 01:24 | Niki’s goal: theorem proving in mainstream programming | | 02:36 | Formal verification explained | | 05:39 | Introduction to refinement types | | 08:06 | Compile-time vs. runtime checks and performance | | 11:05 | SMT solvers and their role | | 13:19 | SMT solvers & Sudoku analogy | | 16:08 | Propagating runtime checks via types | | 19:47 | Dependent types vs. refinement types | | 22:31 | Bringing refinement types to mainstream languages | | 25:57 | Refinement types in Scala & other languages | | 28:15 | Haskell’s advantages for refinement types | | 30:43 | Error reporting and usability | | 34:05 | Proving laws by writing code in Liquid Haskell | | 36:54 | Liquid Haskell as an education tool | | 39:57 | Totality checking and its importance | | 42:07 | Handling divergence (infinite loops) | | 44:51 | Internals: using GHC’s AST | | 47:42 | Verification tools in industry; difference from tests |
Tone & Style
- Conversational, engaging, and accessible—even as the discussion navigates deep technical waters.
- Niki combines academic authority with practical advocacy for making these methods usable in the real world.
- Adam provides grounded, clarifying questions and analogies relevant to everyday programming.
Summary
This episode offers a comprehensive, approachable exploration of refinement types and formal verification for software developers. Niki Vazou demystifies how these tools can be both powerful and practical, their relationship to dependent types and language features, and the technical machinery (like SMT solvers) that make them possible. Throughout, there’s an optimistic vision: as tools like Liquid Haskell mature, formal methods might not just be for experts, but will become an invisible, reliable part of writing correct and efficient software everywhere.