I don't write these sort of programs but my thinking is that 'draw nice' is vague and I would not know what that means and indeed that is a fuzzy spec I would have only thought you needed more clarification on what good or nice here means and it sounds like what you do is actually work out most of what the program has to do and really they have asked you to make them a drawing program with them giving you input along the way.

This indeed could not be formalized by it's very nature. I was not making a claim on the applicability or even the desirability for all programs and I think many people who have not look at it properly overestimate it's applicability.

What I was trying to say is for the subset of programs that one would want to formalize (such as the examples I gave) the task could be much easier if we have formal primitives, including operating system primitives and networking primitives to provide guarantees.

My other point would be that a lot of developers and projects are writing code that could potentially prove properties and benefits could be derived from proving these properties. I would look at middleware programs as some of the obvious ones that could massively benefit from such techniques and formalization (though things like streams can be much more easily formalized and modeled correctly).