I 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.