Verified Programming of Turing Machines in Coq (2020)

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.

[1] https://en.wikipedia.org/wiki/Total_functional_programming

[2] https://kseo.github.io/posts/2015-06-18-total-functional-pro...