The most powerful language I know of is LISP. Guess what one of most field-proven verification tools uses and verifies? LISP via ACL2.<p>There were also hardware kits like DDD that did correct by construction hardware from LISP specs. So, power != hard to verify. One should subset, though, for best results.