3 ms·

The post missed something very important! The whole time I was reading I was thinking to myself “good luck keeping your code error-free after you’re done transc

The post missed something very important! The whole time I was reading I was thinking to myself “good luck keeping your code error-free after you’re done transcoding from Dafny to the language you actually use in-prod” but… The language (Dafny): https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny Dafny is a verification-ready programming language. As you type in your program, Dafny's verifier constantly looks over your shoulder, flags any errors, shows you counterexamples, and congratulates you when your code matches your specifications. When you're done, Dafny can compile your code to C#, Go, Python, Java, or JavaScript (more to come!), so it can integrate with your existing workflow.

redjamjar 3y ago
Yeah, so as I understand it, AWS is using Dafny generated (Java) code in production. I think we can assume it won't be as efficient has hand written code (at this stage anyway) but it does give you the added guarantees.
- ComputerGuru 3y ago
  > I think we can assume it won't be as efficient has hand written code Actually, surprisingly, not necessarily the case! If you'll refer to the discussion in https://github.com/dafny-lang/dafny/issues/601 https://github.com/dafny-lang/dafny/issues/601 and in https://github.com/dafny-lang/dafny/issues/547 https://github.com/dafny-lang/dafny/issues/547, Dafny can statically prove that certain compiler branches are not possible and will never be taken (such as out-of-bounds on index access, logical assumptions about whether a value is greater than or less than some other value, etc). This lets you code in the assumptions (__assume in C++ or unreachable_unchecked() under rust) in the generated production code that will then allow the compiler to optimize the codegen using this information. (Caveat: I just heard of Dafny today. Definitely not an expert!)

redjamjar 3y ago

Yeah, so as I understand it, AWS is using Dafny generated (Java) code in production. I think we can assume it won't be as efficient has hand written code (at this stage anyway) but it does give you the added guarantees.

ComputerGuru 3y ago
> I think we can assume it won't be as efficient has hand written code Actually, surprisingly, not necessarily the case! If you'll refer to the discussion in https://github.com/dafny-lang/dafny/issues/601 https://github.com/dafny-lang/dafny/issues/601 and in https://github.com/dafny-lang/dafny/issues/547 https://github.com/dafny-lang/dafny/issues/547, Dafny can statically prove that certain compiler branches are not possible and will never be taken (such as out-of-bounds on index access, logical assumptions about whether a value is greater than or less than some other value, etc). This lets you code in the assumptions (__assume in C++ or unreachable_unchecked() under rust) in the generated production code that will then allow the compiler to optimize the codegen using this information. (Caveat: I just heard of Dafny today. Definitely not an expert!)