Comment by Sharlin

What even is the most complex programming language with a fully machine-checkable spec? Are there actually practically useful ones? I know of none.