> Languages like Idris and Agda are different because sometimes code isn’t executed at all. A proof may depend on knowing that some code will terminate without running it.

Yes. They are rather different in other respects as well. Though you can produce executable code from Idris and Agda, of course.

> With respect to deadlocks, there’s little practical difference between an infinite loop and a loop that holds the lock for a very long time.

Yes, that's true. Though as a practical matter, I have heard that it's much harder to produce the latter by accident, even though only the former is forbidden.

For perhaps a more practical example, have a look at https://dhall-lang.org/ which also terminates, but doesn't have nearly as much involved proving.