Per the Wikipedia page for Whiley[1] the languages akin to Dafny are mentioned when explaining what Whiley is: “The primary purpose of such a tool is to improve

Per the Wikipedia page for Whiley[1] the languages akin to Dafny are mentioned when explaining what Whiley is: “The primary purpose of such a tool is to improve software quality by ensuring a program meets a formal specification. In other words, to help identify and eliminate software bug in the programs being developed. Whiley follows many attempts to develop such tools, including notable efforts such as SPARK/Ada, ESC/Java, Spec#, Dafny, Why3 and Frama-C.” I'm thinking there must be a reason they do not mention F*, Coq, Agda, and Idris, perhaps because they are proof assistants[2] rather than automatic provers of programs with formal specifications. See also Isabelle and others. Regarding Idris (which you mention but is not on that page) and Epigram (which is noteworthy and again not on that page), neither are production ready and the latter is unmaintained. [1] https://en.wikipedia.org/wiki/Whiley_(programming_language)#Overview https://en.wikipedia.org/wiki/Whiley_(programming_language)#... [2] https://en.wikipedia.org/wiki/Proof_assistant https://en.wikipedia.org/wiki/Proof_assistant