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".