I would like to Add my Beads language to your list. if you avoid the intentional escape hatch untyped constructs which are only used for interfacing with external systems, Beads programs are strongly typed, sound, and in normal programs 100% verifiable for type correctness at compile time. we have an extended arithmetic which is closed, which greatly simplifies the issue.

regards,

edward de jong magicmouse94937@gmail.com beadslang.com