Steel:wishlist

This page is a list of shortcomings of Low*v2 that we absolutely would like to address with STEEL, and in particular the redesign of the user programming model.

size_t

The array type needs to have its length defined over an abstract module of size_t. size_t will be similar to a machine integer, in that it supports arithmetic operations. However, its maximum value will be unspecified.

Injections from machine integers will be made available, at the expense of generating static asserts in the generated C. We regroup all of the target assumptions in a module called Steel.Target which will expose:

module Steel.Target

val size_at_least16: bool
val size_at_least32: bool
val size_at_least64: bool

val little_endian: bool

These will be defined by hand using compiler macros.

val size_of_uint16: x:UInt16.t { Steel.Target.size_at_least16 } -> y:size_t { v y == v x }