Tech Talk: Idris, Proofs and Haskell with Edwin Brady
CoRecursive: Coding Stories
00:00
The Language Strangeness Budget
In idres, it will always check whether something is total. So i take by implication, er idrses ae total language as a always total, or it's not always total. But there is this goal of being accessible to the more main stream software developers and bringing it closer to what people do in practice. I think you knowit once. Once the tools are better fora detecting where the programms are terminating a this, i it, it's going to be just like a yokno.
Transcript
Play full episode
