MoonBit 0.9: Introducing First-Class Formal Verification
3 points by hongminhee
3 points by hongminhee
I don't really see a clear difference between languages like Dafny and F* with MoonBit as the article suggests. Don't all of them have proofs baked into the language and designed to generate executable code?
To my admittedly cursory knowledge, MoonBit descends from Rust. The language is adding new verification features on top of a Rustlike, whole Dafny and F* are designed for verification from the start.