Re:Programming Languages Going Above and Beyond
by redjamjar on Thursday June 29, 2023 @05:23PM
(#36526930)
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.
Re:Programming Languages Going Above and Beyond
by ComputerGuru on Thursday June 29, 2023 @06:26PM
(#36527674)
> 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 and in 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!)
The language (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.