Tech Talk: The Little Typer With Daniel Friedman and David Thrane Christiansen
CoRecursive: Coding Stories
00:00
Is There a Correspondence Between Programming and Proofs?
A total function is a function if every element of the domain is paired up with exactly one element of the range. In order for all our programmes to correspond to proofs in pie, we make sure that you can only write total functions. And these elimination forms, like the inanat that you ware talking about earlier, those allow you to make sure both that your cov ing all the possible gnats and that any recursion you do is controlled in such a way that recursive calls are all happening on one smaller number. If we allowed recursion, i don't know, when ikon programming in scalar terms I tend to use like dreccrec or let's say fold
Transcript
Play full episode
