Thank you for the example.

Also: SPARK is another one I forgot. I guess I'll have to think of a nice example and just implement it in a Ada, F* and with RDL to get a hang of the differences and features.