> I mean would you take that spec as something you could deliver?

Yes, that's the kind of contract we take on regularly. My point is that the exact thing the customer wants/needs is the one part that can't be formalized meaningfully - it's good when we show them something and they tell us is good. Everything else doesn't matter - could be the worst UI, maybe you have to reboot the computer once before starting it and once after exiting it, maybe it leaks enough memory that you have to reboot every day anyways - what matters for them to pay you is "do they like the drawing quality" and really nothing else

> Yes, that's the kind of contract we take on regularly. My point is that the exact thing the customer wants/needs is the one part that can't be formalized meaningfully

I think that's fine though. The exact fuzzy thing the customer wants is typically still built on top of a ton of stuff that can be verified. I'm not sure it needs to be either-or. You formalize what you can, and do your best with what you can't. Ideally (if we could find a way to make formalized software cheaper/easier to build) it would reduce time wasted on the stuff that can be formalized, and allow spending more time on the stuff that can't be.

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).

The contract may be that, but then as part of that contract you work together with the client, using your experience and foresight to actually create a more detailed "spec". That is still not completely formalized, but your developers/colleagues using their experience in other projects can "draw the rest of the owl" from that semi-vague spec -- and the final delivered software is the spec itself in a way.

It's absolutely not impossible to simply add one more layer in-between the developers "drawing the rest" and delivery. They just not formalize it as software in one go, but "in two".