2 ms·
Verified Programming of Turing Machines in Coq (2020)
- maxsun 6y agoI was recently reading into Total Functional Programming [1] and found it surprising that it seems possible to reason about/model Turing Machines in languages which guarantee a program's termination [2]. I've barely scratched the surface, but I feel like it's a fun combination of engineering and theoretical/philosophical issues. I'd super appreciate and fellow HNers suggestions for related resources or things to read. [1] https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming [2] https://kseo.github.io/posts/2015-06-18-total-functional-programming.html https://kseo.github.io/posts/2015-06-18-total-functional-pro...