A statically typed programming language that unifies implementation with formal specification