alt Hacker NewsI got a bit into SPARK (a subset Ada of that has formal verification) with AoC, and while it can be tricky, SPARK is quite flexible in how much you prove. Dafny sounds interesting, but I can't find a comparison between the two. There's obviously a difference in memory management, but the rest looks quite similar at first sight, and their niche is quite similar. Does anyone know of a (deeper) comparison between both languages?
One difference is that SPARK is intended primarily for safety critical, real-time software (often for embedded systems), while Dafny is meant for teaching purposes and non-real time applications (i.e. environments where a large runtime and garbage collection are permissible). Dafny compiles to C#/Java/Go/etc. and is meant to be interoperable with them so I think it aims at similar use cases as those languages.