Minimally typed programs?

I wonder whether there is work on the idea of minimally typing a program. Assume that I have a program and a property I wish it satisfies. Is there a way to derive the least amount of typing to apply to the program such this property is satisfied?