Features.md

Feature	C#	JavaScript	Go	Java	Python	C++	Dafny Library (.doo)
Unbounded integers	X	X	X	X	X		X
Real numbers	X	X	X	X	X		X
Ordinals	X	X	X	X	X		X
Function values	X	X	X	X	X		X
Iterators	X	X	X		X		X
Collections with trait element types	X	X	X	X	X		X
External module names with only underscores	X	X		X	X	X	X
Co-inductive datatypes	X	X	X	X	X		X
Multisets	X	X	X	X	X		X
Runtime type descriptors	X	X	X	X	X		X
Multi-dimensional arrays	X	X	X	X	X		X
Map comprehensions	X	X	X	X	X		X
Traits	X	X	X	X	X		X
Let-such-that expressions	X	X	X	X	X		X
Non-native numeric newtypes	X	X	X	X	X		X
Method synthesis	X						X
External classes	X	X	X	X	X		X
Instantiating the object type	X	X	X	X	X		X
forall statements that cannot be sequentialized1	X	X	X	X	X		X
Taking an array's length	X	X	X	X	X		X
m.Items when m is a map	X	X	X	X	X		X
The /runAllTests option	X	X	X	X	X		X
Integer range constraints in quantifiers (e.g. a <= x <= b)	X	X	X	X	X	X	X
Exact value constraints in quantifiers (x == C)	X	X	X	X	X		X
Sequence displays of characters2	X	X	X	X	X		X
Type test expressions (x is T)	X	X	X	X	X		X
Type test expressions on subset types							X
Quantifiers	X	X	X	X	X		X
Bitvector RotateLeft/RotateRight functions	X	X	X	X	X		X
for loops	X	X	X	X	X	X	X
continue statements	X	X	X	X	X	X	X
Assign-such-that statements with potentially infinite bounds3	X	X	X	X	X	X	X
Sequence update expressions	X	X	X	X	X	X	X
Sequence constructions with non-lambda initializers4	X	X	X	X	X	X	X
Externally-implemented constructors	X			X	X	X	X
Auto-initialization of tuple variables	X	X	X	X	X	X	X
Subtype constraints in quantifiers	X	X	X	X	X	X	X
Tuples with more than 20 arguments		X	X		X	X	X
Arrays with more than 16 dimensions		X	X		X	X	X
Arrow types with more than 16 arguments		X	X		X	X	X
Unicode chars	X	X	X	X	X		X
Converting values to strings	X	X	X	X	X		X
Legacy CLI without commands	X	X	X	X	X	X
Separate compilation	X		X	X	X	X	X
All built-in types in runtime library	X	X	X	X	X		X
Execution coverage report	X
Standard libraries	X	X	X	X	X		X
Standard library ActionsExterns	X			X			X

Footnotes

1. 'Sequentializing' a forall statement refers to compiling it directly to a series of nested loops with the statement's body directly inside. The alternative, default compilation strategy is to calculate the quantified variable bindings separately as a collection of tuples, and then execute the statement's body for each tuple. Not all forall statements can be sequentialized. ↩

2. This refers to an expression such as ['H', 'e', 'l', 'l', 'o'], as opposed to a string literal such as "Hello". ↩

3. This refers to assign-such-that statements with multiple variables, and where at least one variable has potentially infinite bounds. For example, the implementation of the statement var x: nat, y: nat :| 0 < x && 0 < y && x*x == y*y*y + 1; needs to avoid the naive approach of iterating all possible values of x and y in a nested loop. ↩

4. Sequence construction expressions often use a direct lambda expression, as in seq(10, x => x * x), but they can also be used with arbitrary function values, as in seq(10, squareFn). ↩