I can still hear "whoosh" in my own ears here 8) Given how simple a Turing Machine can be, I seriously doubt (without any proof) that coq is not able to recrea

I can still hear "whoosh" in my own ears here 8) Given how simple a Turing Machine can be, I seriously doubt (without any proof) that coq is not able to recreate a TM. I am not an expert but the explanation about Turing Machines I read was in GED and involved a simple tape and a slack handful of symbols and operations and some basic hand waving. If coq can't manage that then it is unlikely to be useful - which I doubt.