This is a very interesting idea. The world needs more languages that make formal provability practical. And I think I found a typo: thery is_open(int*) -> bool

This is a very interesting idea. The world needs more languages that make formal provability practical. And I think I found a typo: thery is_open(int*) -> bool; -- should be "theory".