By Adam Gordon Bell - Software Developer
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...