Can one prove that "hello, world" printed in two different ways has the same effect in Dafny?

Question

It seems intuitively clear that the effect of the following two methods are identical, if one ignores intermediate stages:

method print1()
{
    print "hello, world\n";
}

method print2()
{
    print "hello, ";
    print "world";
    print "\n";
}

Is there a way to assert the equivalence of side effects for these two methods?

Answer 1

No, there's no builtin way to do this.

Even if there was, it wouldn't support the many operations not built in to Dafny that are needed to connect a program to the real world, such as reading input.

If you want to do something like that, the way to do it is to build a logical model of the aspects of the side effect that you care about capturing, and then axiomatize the fact that the primitive operations satisfy their specifications.

(You might find this unrelated answer about file IO useful as a starting point, but it does not address the question of logical modeling.)