C# runtime's tuple deconstruction incompatible with .NET Framework pre-4.7

[alex-chew]

The C# runtime in Dafny v3.5.0 uses tuple deconstruction (see first and last lines):

dafny/Source/DafnyRuntime/DafnyRuntime.cs

Lines 1192 to 1203 in 76c8d59

	var (leftBuffer, rightBuffer) = (left, right);
	if (left == null || right == null) {
	// elmts can't be .IsDefault while either left, or right are null
	return elmts;
	}
	toVisit.Push(rightBuffer);
	toVisit.Push(leftBuffer);
	while (toVisit.Count != 0) {
	var seq = toVisit.Pop();
	if (seq is ConcatSequence<T> cs && cs.elmts.IsDefault) {
	(leftBuffer, rightBuffer) = (cs.left, cs.right);

This is problematic because it fails to compile on .NET Framework versions below 4.7, which are missing runtime support for this feature:

error CS8179: Predefined type 'System.ValueTuple`2' is not defined or imported [/home/runner/work/Foobar.csproj]
error CS8130: Cannot infer the type of implicitly-typed deconstruction variable 'leftBuffer'.
error CS8130: Cannot infer the type of implicitly-typed deconstruction variable 'rightBuffer'.
error CS8179: Predefined type 'System.ValueTuple`2' is not defined or imported

This seems to be a known issue that can be worked around either by manually deconstructing the tuple, or by depending on the System.ValueTuple package.

[alex-chew]

To add some context - we want to support .NET Framework 4.6.2 because Microsoft hasn't announced an end-of-support date: https://docs.microsoft.com/en-us/lifecycle/products/microsoft-net-framework

[texastony]

Ideally, Dafny would advertise the details of the supported compiled languages:
i.e.: Dafny's compiled output uses features from JavaScript X, Java Y, Go Z, etc.

[cpitclaudel]

Ideally, Dafny would advertise the details of the supported compiled languages:

Or even better it would target a version so old that this issue doesn't even pop up

[alex-chew]

Ideally, Dafny would advertise the details of the supported compiled languages:

Or even better it would target a version so old that this issue doesn't even pop up

Regardless of the age of language runtime versions that Dafny supports, I'd still prefer that Dafny be explicit about which versions it supports.

[alex-chew]

(To clarify, the workaround of depending on System.ValueTuple works fine for us, and we're not in a rush to remove that workaround.)

[robin-aws]

Ideally, Dafny would advertise the details of the supported compiled languages:
i.e.: Dafny's compiled output uses features from JavaScript X, Java Y, Go Z, etc.

Split off #1983 to track this as a separate and actually more important ask.

[atomb]

I believe that this issue is fixed. Looking at the latest version of the runtime, it no longer uses tuple destruction. We're also building the runtime for framework net452, which I would imagine would fail if we were using features introduced more recently.