A really interesting and clear iterview! Thank you.
That stack usage static analysis is interesting. Does it have a way of verifying that the C annotation is correct, or is that a matter of trust? Also does the static analysis behave differently on different platforms? As stack sizes may be different.