3 ms·
If you don't want to install anything, you can get a taste of Dafny by looking at its online tutorial. https://rise4fun.com/Dafny/tutorial https://rise4fun.com
by dwohnitmok 6y ago
If you don't want to install anything, you can get a taste of Dafny by looking at its online tutorial.
https://rise4fun.com/Dafny/tutorial https://rise4fun.com/Dafny/tutorial
Dafny is a good example of what formal verification looks like for imperative languages (as opposed to e.g. dependent types for functional languages). Gotta love loop invariants!
- mcguire 6y agoDafny (and formal verification for imperative languages) is a lot of fun. But does Dafny have any library documentation? Is it .Net?
- dwohnitmok 6y agoI'm not quite sure what you mean. Dafny compiles to .NET indeed. What do you mean by library documentation? Dafny doesn't have many (any? I certainly haven't used any...) libraries to begin with.
- mcguire 6y agoI thought Dafny has access to the .NET infrastructure. But when I played with Dafny a while back, the only library interface I saw was printing to stdout (IIRC), which would imply that Dafny was a toy language intended for playing with verification and not much else. On the other hand, I've heard otherwise---it's been used for Windows drivers?---but without any documentation or examples, I lost interest.