[anyfoo]

That is not too far from what proof assistants actually do.

Agda is a dependently typed language (strongly resembling Haskell in Syntax, but with a lot more Unicode) where you rarely, if ever, "run" your programs but rather just check if they "compile", i.e. type check. If it does type check, you proved what you set out to prove.

Its standard library contains a lot of stuff you'd need for basic proofs: https://agda.github.io/agda-stdlib/