I mean would you take that spec as something you could deliver? This is not a real problem spec and is incredibly vague, but the first question would be around building a formal model for the drawing part of the application (and is the main aspect of the program) that might be easier then it first seems. There are various ways you could model the draw window depending on if it's a rasterizing program or a vector program either way not challenging, then formalize the operations of the program (various effects will necessary be well defined mathematical functions in the first place) and then prove what ever you feel you have to prove about the system. This is not to say it is easy or especially in this case you should even do it and my point was more about the system aspect of things or things that one would want to be able to reason about.

An example of a spread sheet program might have been more productive example or a http API server or some kind of middle where program. I feel like you picked the most obtuse example possible even though my point was not to cover all possible programs that one might want to write.

▲

jcelerier an hour ago | parent | next [-]

> 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

▲

kodoman 35 minutes ago | parent [-]

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

	▲	bluGill 10 minutes ago \| parent [-]
		I don't write those sorts of programs either. There is evidence that some people do write that sort of program with varying amount of success in "draw nice". I'm sure such people could write books on what draw nice means. I would refuse such a job because I don't have the right expertise, and you probably wouldn't hire me for it even if I would accept it. However hire the right expert and you can probably get what you want even though at the start you don't even know what you really want - the other option is the expert will quickly realize is what you want is not what they can do and either tell you not to waste your money or warn you that you are going to spend a lot of money on an open ended research project that may or may not produce results.

▲

bluGill 34 minutes ago | parent | prev [-]

That is very common for something given in the industry. It is our job as programmers to first figure out what the customer really wants, and then create enough of the requirements/spec to deliver it. That is one of the reasons for Agile vs Waterfall processes: nobody really knows what they want in the first place so you deliver something that you think is close and work with them to come up with something acceptable (acceptable covers both it does what they want, and also the cost to make it better). Any formal spec needs to be adjustable as we figure out requirements.

OTOH, we can probably call a much less formal spec good enough. Just that it doesn't write past the end of buffers would be very helpful. We can also throw a bounds in - if we can't prove it in X iterations then call it false (expect to adjust X to very large)

	▲	kodoman 10 minutes ago \| parent [-]
		Not that vague first you need to know what the customer means by good. I was not making claims on the applicability of formal methods any way, only the point I was making about the primitives.