It seems I scanned the pages too quickly -- there exists an alloc_array
for arrays and alloc for pointers (see page 9 of the language
reference), but there is indeed no free (but garbage collection).
The alloc_array returns an array and can be used only once when the variable is declared.
And as you have noticed, there is no free. So we can't call it a memory management. The
same applies to alloc for pointers.
There is no casting, no pointer arithmetic, no memory management. All what can
make the program difficult to prove has been removed.
Nice teaching idea.
--
FL