Tech Talk: Idris, Proofs and Haskell with Edwin Brady
CoRecursive: Coding Stories
00:00
Programming Languages Aren't Computable, but You Could Write Packman in Them
Programming languages are incomplete, but can still be used to solve computable problems. Theory provers require programs to be a total which means they need to cover all well typed inputs. But the question is what kind of useful things can you do with this? And i haven't yet found a useful thing by disallowing programms looping forever and not producing any output on the way.
Transcript
Play full episode
