ACSL (Ansi C Specification Language), is a specification for C code, annotated with special comments, that allows C code to be formally verified.
I have not looked into it, but I imagine that the formal methods used in ACSL verifiers would be similar to Hoare Logic. For pure functional languages though, such as Haskell, I can't imagine what sort of formalism would be used for formal verification.
Has anyone made something similar to ACSL, but for a pure functional language? If not, has there been any research into specification-annotated style formal verification for functional languages?
I know that there's dependent typing, which many languages (Agda, Idris, etc...) support, but in Haskell dependent typing is difficult without doing some (unreadable?) type-wizardry. With that in mind, and since Haskell has so much better library support than Agda and Idris, I believe such a system for functional formal verification might be useful, but I don't know if research has been done on this or not.