Comment by throwaway17_17

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.