Open alexporter8013 opened 4 months ago
alexporter8013
commented
3 months ago To the end of this issue, I have created lorrel-py. I haven't done much yet, but I would recommend doing something similar for the other supported back-end languages. I would also invite discussion here and PRs for lorrel-py for discussion and suggestions.
robin-aws
commented
3 months ago Hi Alex! Thanks very much for taking the time to write this up, and for the enthusiasm to push for this improvement!
This deserves some deeper discussion, but let me at least respond to your points and provide some background on the current status and what's already in the works:
- Establishing detailed user stories and acceptance tests for integration of Dafny into projects based on other languages. Specifically, and most importantly, I would propose creating example projects in each available back-end language that demonstrates how to incorporate Dafny code inside the parent code base.
I do agree it would be great to have a full example of integration for each target language. What we do have is some great examples of building Dafny code into reusable libraries in other languages, which can then obviously be used in other code bases without even being aware of Dafny, thanks to the AWS Crypto Tools team:
Even then, those projects are designed to be multi-target libraries, where the priority is supporting integration with many different langauges from the same code base. It is also worthwhile to shoot for easy integration of Dafny into existing code bases in a single language at a time as easily as possible, although the language and tooling support for both cases will definitely overlap.
- I would propose publishing Dafny and the Dafny runtime in the package ecosystems for applicable languages. For instance, publishing Dafny on pypi.org for use in build systems, and publishing the Dafny runtime for use as a project dependency in those projects.
We're definitely on top of this!
Still need to publish the runtimes in the other languages but that's on the backlog. But I think you're right that the documentation could emphasize the use case of translating Dafny to other target languages more, which would make it more obvious.
(unless use in other languages is considered a core feature).
It absolutely is.
alexporter8013
commented
3 months ago Hey Robin! Thank you for the detailed reply!
I do agree it would be great to have a full example of integration for each target language. What we do have is some great examples of building Dafny code into reusable libraries in other languages, which can then obviously be used in other code bases without even being aware of Dafny, thanks to the AWS Crypto Tools team:
I took a look through the linked repositories, and I can't really discern how one would use those as a jumping off point for their own integration of Dafny into their project. From what I can tell, those are really designed to fit into a larger AWS ecosystem (I'm not personally very savvy for AWS technologies). So, in-line with creating examples in the different target languages, I think I may be able to make a pretty strong example for Python and start one for C++. I'm not very proficient in project wrangling for any of the other target languages (I've used C#, but only here and for Unity).
We're definitely on top of this!
Excellent! I was misled by #3127, so I appreciate you closing that out.
In my endeavors for working through my own attempt at integrating Dafny into a larger Python project, I have identified a couple of findings. I will the most apparent ones here, and then we can decide if they should be split into different issues or not.
Findings:
dafny translate and dafny compile, except dafny compile will include the standard libraries' code.dafny translate and dafny compile, the generated folder can't be directly imported due to being named with a hypen. The result of this is that any build process would be required to rename the generated folder to make it valid. Also, the output directory cannot be directly named to the user's preference, as the target language abbreviation is always appended with a hyphen, e.g. translated-py.{:extern} on Dafny functions or methods, these extern'd items don't seem to appear anywhere in the output (this one is most likely user error, but then I can just blame documentation - constructively, of course :P).module_.py:
import sys
from typing import Callable, Any, TypeVar, NamedTuple
from math import floor
from itertools import countimport module_ import dafny import System
class default: def init__(self): pass
@staticmethod
def add(x, y):
return (x) + (y)
5. The generated code causes many lint warnings and errors, in addition to discouraging manual review due to the previously mentioned naming as well as formatting. I not sure how mature the translation is considered, but I would prioritize humans in the loop as much as possible until the translation is quite mature.
I have some sizable roadblock for the "actual" example of integration of Dafny into a larger project, thus I will focus my future efforts into making an "ideal" example. After the "ideal" example is established, I will ask for help in what it would take using the current implementation model to generate the same or similar result.
As a side note, linters complain a lot about the generated Python code. This would further complicate integration into other build processes since all of the generated files would essentially need to be ignored.I have finally fleshed out a prototype for Dafny integration into larger Python projects here. I would appreciate any time that can be taken to review what I have put together.
Summary
Define detailed user stories and CONOPs for users who would like to use Dafny as a part of their larger code base.
Background and Motivation
Dafny supports various back-ends for things translation, compiling, and execution, but the current feature set seems to lack coherence and do not provide straightforward models of Dafny integration into larger code bases. For instance, when translating to Python, the documentation doesn't mention which version of Python is being targeted, nor does Dafny allow the user to specify such.
Proposed Feature
Establishing detailed user stories and acceptance tests for integration of Dafny into projects based on other languages. Specifically, and most importantly, I would propose creating example projects in each available back-end language that demonstrates how to incorporate Dafny code inside the parent code base.
I would propose an overhaul of the documentation concerning these activities.
I would propose publishing Dafny and the Dafny runtime in the package ecosystems for applicable languages. For instance, publishing Dafny on pypi.org for use in build systems, and publishing the Dafny runtime for use as a project dependency in those projects.
Proposal 1 takes the highest priority as it would inform the direction on proposals 2 and 3. Most importantly is figuring out how a user wants to use Dafny in their larger code base, then we can catch Dafny up to support that CONOPs.
Alternatives
The current model is technically workable, as such this proposal should be considered an enhancement to improve adoptability of Dafny, not necessarily to improve its performance or core feature set (unless use in other languages is considered a core feature).