If you are asking in the context of Idris 2.0 (the current version), ST is not really related.

However, if you mean ST in Idris 1.0, there is a definite correlation. The mechanism that ST used for enabling local mutations was very similar to the mechanism that the typestate pattern in Rust is using. ST was a framework for formalizing State Machines in dependent types which is the mechanism TFA is analyzing.

This is not really ST. This is analogous to eating at an old school restaurant.

You can't just walk in to the food service counter and say "give me a burger"; you need to first get a ticket from the cashier proving that you've ordered a burger and then provide that ticket to the guy at the counter.

That's literally the type state pattern

Yes, I believe it should be possible for someone to do that.