Comment by sprinkly-dust

F-Star and Dijkstra Monads (which are apparently not really monads?) might get you to what you're looking for