Here[1] is a note by Dijkstra that goes into formally constructing correct programs in a language with built in nondeterminism. Nondeterminism is a powerful tool, not just a foot gun.

[1] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/E...

further along those lines: https://en.wikipedia.org/wiki/UNITY_(programming_language)

(note that regexps can also —exponentially— leverage nondeterminism)