For that you would need a proper, well-grounded type system and a language that doesn’t stray from it.

Some fp languages are close enough to fit that bill; Rust too is going down this path: its type system was built to make a proof, after all.