Request: very basic file I/O

[robin-aws]

I've been intentionally cautious about this, since it requires linking to external code in each language no matter how you slice it. But I think the timing is right to experiment with very basic methods for reading and writing files, without streaming and without any model of the file system.

Since this repo contains only "pure" Dafny logic and no externs, I assert the I/O should go into a separate repo. That way we can continue to support consuming this repo as a simple submodule, whereas the I/O library will have to be packaged together with native code in some way.

[parno]

FWIW, I'd be a bit nervous about undertaking this at at moment when everyone seems to agree that extern is currently somewhat broken (e.g., dafny-lang/dafny#2397, dafny-lang/dafny#469, dafny-lang/dafny#313, dafny-lang/dafny#2291), but we haven't yet converged on a new approach. You may be bolder than I am, however :)

[hmijail]

Not sure where to ask this, but I guess here it's on point.
I see that the file I/O implementations were merged in but with Go "out of scope" because of bugs in fundamental aspects of translation of Dafny to Go.
Those bugs seem pretty related to a bunch of others that I have reported myself.

My team is considering moving forward with a Go translation of Dafny code, and for now I've been finding my own workarounds for those bugs. But this "out of scope" makes it sound like maybe this isn't a good idea after all. Would it be possible to get some clarity on what is the status of Go support? For example, any timeline regarding when would a Go file I/O implementation be added?

Please let me know if this question makes more sense elsewhere.

[alex-chew]

Hi @hmijail, thanks for reaching out. We intend to support the Go compiler at the same level as the others. We don't have a concrete timeline for adding a Golang file I/O implementation, but for now you can track this work here: #79

I would say that of the two blocking issues I linked in #60 (comment), only the former (dafny-lang/dafny#2989) is a fundamental issue in the Go compiler, and fixing this kind of bug is indeed a priority for us. It's one we intend to fix as we work on improving the interoperability between compiled Dafny code and code written in target languages.

The latter issue (dafny-lang/dafny#2045) is easily worked around if you're only compiling to Go. That workaround was insufficient for this PR only because we needed a single Dafny {:extern} declaration that works "the same" across all languages, and Golang is an odd one out. Again, we expect to improve or eliminate this edge case as we improve Dafny interoperability.

[robin-aws]

@parno:

FWIW, I'd be a bit nervous about undertaking this at at moment when everyone seems to agree that extern is currently somewhat broken (e.g., dafny-lang/dafny#2397, dafny-lang/dafny#469, dafny-lang/dafny#313, dafny-lang/dafny#2291), but we haven't yet converged on a new approach. You may be bolder than I am, however :)

Absolutely a fair point. We're relying on the fact that the implementation of the file I/O is well encapsulated, so if and when we have something that works better than {:extern} currently does, we can move to it without breaking any consumers.

[hmijail]

The latter issue (dafny-lang/dafny#2045) is easily dafny-lang/dafny#2045 (comment) if you're only compiling to Go.

That's not a problem I have found myself yet, but I'll keep it in mind just in case :). Though we do hope to keep multiple target languages, so it's not ideal.