[deterministic]

Completely agree. Refinement types is a much more practical tool for software developers focusing on writing real world correct code.

Using LEAN or Coq requires you to basically convert your code to LEAN/Coq before you can start proving anything. And importing some complicated Hoare logic library. While proving things correct in Dafny (for example) feels much more like programming.