Is the Dafny to Python code certified? If so, why does not Python have native pre-post options? If not, why translate it?

Question

I have recently started testing with the Dafny to Python compiler dafny build --target:py A.dfy offered in its latest version. I'm not sure if it "works well", because it doesn't generate all the functions I have in Dafny (is this normal?).

However, I have a rather "philosophical" question about the use of translating a Dafny file into a Python file. Essentially, the Dafny code is a "certified" code in the sense that it guarantees that the functions fulfill their properties (if pre, then post); my question is, does the Python code fulfill this same thing?

If the answer is yes, the question is: why is not "certified" code written in Python? I mean why does not Python have some kind of native pre, post and assert (not the assert of Python). If the answer is no, the question is: what is the point of translating "certified" code to a "non-certified" one?

Answer 1

Only the executable code, but not the specifications are compiled. functions are not, whereas function methods are. Check the reference manual for more details on that. If you find that what is documented to work is not in line with what you experience, consider opening a ticket.

The translation to Python is meant to preserve the semantics of your program. As this process isn't verified, there is no way of knowing that it does do that in all circumstances. Extending a language like Python with the necessary constructs for contracts and writing a verifier for the whole language sounds like a tall order, but this is ultimately a question for the Python community, not us. The point of compilation is that it lets you run your Dafny programs. If we would compile down to Assembly, you probably wouldn't worry about preserving the specifications.

• Theo Deep: As for the first paragraph, I just checked and you are right: some functions that I intented to be function method are function, so I must correct that. As for the second one, I think I do not understand it :( I mean, my problematic is as follows: I have a Python program and I want to call a verified code in Dafny; however, since this code will be called thousands of times (and this has a parsing-cost and other costs), I considered translating Dafny to Python... but I am not sure if this translated code preserves the (Hoare-like) guarantees that the Dafny code offered. Any idea?
• user14704889: If you were to remove the specifications from your Dafny code, the semantics wouldn't change, so the presence of specifications in the Python code doesn't make a difference either. The critical part is the correctness of the compilation/translation, but that affects you both when you run your code through the Dafny CLI, or interface with the compiled code directly.
• user14704889: This is only a problem if you alter the code after stripping the specs, but that's not the intended workflow. If you need to change the compiled code, you should change the Dafny code and recompile.
• user14704889: Check out the documentation on {:extern} in case you need to use some target language code.
• user14704889: When you declare {:extern} code, you can add specifications using pre- and postconditions, but Dafny will treat those as axioms, as it has no way of reasoning about code written in another language. This is the kind of code the reference manual is concerned with here. To borrow the language of the manual, my comment was about Dafny-originated code. My point is that once you start changing that generated code by hand, all promises we make about the correctness are rendered moot.