In programming, the closest I’ve seen to a widely practiced theory has come out of the Haskell community. There, you can see the beginnings of a theory in which programs are constructed out of formal building blocks like monoids and functors and where appeals to category theory and monad laws guide design decisions.
It’s a start.
I also really can't get away without mentioning Edward Kmett, Conal Elliott, and Edward Z. Yang for writing both blog posts and code expanding on the practical advantages of theoretical methods.
 https://personal.cis.strath.ac.uk/conor.mcbride/ further work available extensively at StackOverflow, user Pigworker (http://stackoverflow.com/users/828361/pigworker) and you should definitely attempt to read Kleisli Arrows of Outrageous Fortune if you're interested in some dependently typed madness.
 http://www.haskellforall.com/ and especially http://www.haskellforall.com/2012/09/the-functor-design-patt...
And there's the inimitable Luke Palmer , whose blog contains nuggets of gold for those who care to dig through the archives.
Most of the intuitions of programming are not provable and will not become provable, ever. I think I can back that up using the properties of the arithmetical hierarchy from Yu I. Manin.