Safety is commonly implemented via strong static typing. Although there are very powerful type systems (dependent typing), none of them are powerful enough to express arbitrary formal proofs about code. Another problem is that type systems are tightly coupled with a single programming language, inhibit formal proofs refactoring.
One possible framework I am thinking is a compiler that activate optimizations when programmer (or an automated tool) provides formal proofs that allows them. Examples are uniqueness, termination, array bounds checking, memory management, safety, etc.
Is there any programming language that implements in some way this concept?
I am aware of proof carrying code, but it is normally implemented as a conventional type system and a compiler that proves type safety under program transformation.
The code generator for the Isabelle/HOL proof assistant is based on the principle you describe. One can specify an abstract relation that is given in a declarative way, meaning that there is no effective algorithm to check that it holds for arbitrary input (though it might be possible to prove it for some specific inputs). Then one defines a function to check that the relation holds or not for arbitrary values. This includes some steps to ensure that the function is computable, e.g. to show that it terminates. Next, one proves that the relation and the function can indeed be used in place of each other. Finally, with this proof, it becomes possible to tell Isabelle that the function can be used to generate code (in one of supported functional languages) for the original predicate.
Of course, if there are two such functions, a preferred one can be selected for code generation. This can also be viewed as an optimization that produces provably identical results.