CoRecursive: Coding Stories

By Adam Gordon Bell - Software Developer

Refinement Types and Liquid Haskell With Niki Vazou

Published May 15, 2019 4:00am

Formal verification and type systems - how do they relate? Niki Vazou is on a mission to bring better formal verification to the masses.

I have done a couple of episodes about dependent types and my feeling is that dependent types are super powerful and have some conceptual simplicity ( Types are a first-class concept ) but are somewhat tricky to wield in practice.

Refinement types are something simpler. A refinement is a predicate that narrows the meaning of a type. What if instead of divide taking two ints, one was Int i where i != 0. This is...