Agile Game Development

Do any game projects use Formal Proofs?

Philippa Cowderoy wrote:

> Taken with excessive formalism, pretty painfully. If you've got a language
> with a good type system, lighter weight versions (ie skipping half the
> working, not showing any of it) can be pretty effective - but then it also
> starts to sound a lot like an effective coder simply doing what they do.
> Or maybe I have a biased sample due to the number of FP folks I talk to?

Ah, the old "my proof can beat up your proof" methodology.

FP is used in life-critical systems. Here's a great post by one of its
thought leaders:

Rod Chapman wrote:

> John Roth wrote:

> > The thing to understand is that the latter facility is critical:
> > to do TDD, the language system (including the prover)
> > needs to be able to cycle within a few seconds.
>
> Absolutely. If I can be so bold as to quote myself:
>
> "The efficiency of any such analysis is crucial. If you want someone to
use
> a tool in preference to compiling and testing, then the tool must be fast!
> Again, the intractable nature of many static analysis problems on
> traditional languages has limited the adoption of these tools."
>
> Basically, SPARK is very carefully designed so that all the analyses
> are sound and computable in Polynomial time. The Examiner can do its
> static semantics and information flow analysis very, very fast - a couple
> of seconds for a single body is typical. Analysis of the entire
> Examiner (about 60kloc) takes about 2 minutes on a modest PC.
>
> Theorem proving is not quite so fast, but not too shabby either -
> we have a 20kloc system here that generates about 18000 proofs.
> The prover takes about 43 minutes to churn through those on a
dual-processor
> P4 box. This brings "regression proof" into scope for reasonable size
> embedded projects at least in a lunch-time or overnight time-frame.
>
> - Rod Chapman, SPARK Team, Praxis Critical Systems

Notice Rod's team tuned their system for rapid turnaround.

--
Phlip
http://industrialxp.org/community/bi...UserInterfaces

On Mon, 22 Nov 2004, Phlip wrote:

> Do any game projects use Formal Proofs?
>

I know a couple of folks who've bashed that out at the design stage,
though IIRC they tend not to prove the final code. Generally this is when
they've been working out something that's mathematically intense.

> Philippa Cowderoy wrote:
>
> > Taken with excessive formalism, pretty painfully. If you've got a language
> > with a good type system, lighter weight versions (ie skipping half the
> > working, not showing any of it) can be pretty effective - but then it also
> > starts to sound a lot like an effective coder simply doing what they do.
> > Or maybe I have a biased sample due to the number of FP folks I talk to?
>
> Ah, the old "my proof can beat up your proof" methodology.
>
> FP is used in life-critical systems. Here's a great post by one of its
> thought leaders:
>

Believe it or not I follow an amount of this stuff - it's pretty much my
subject at uni, though I'm still nominally an undergrad. There're ways and
means, certainly - dependant types are starting to look seriously
interesting (have a play with something called Epigram), and it's
reasonably easy to catch a shockingly large number of errors at
compile-time with some of the more modern derivatives of the
Hindley-Milner type system (yes, I'm working on one bit-by-bit).

--
flippa@flippac.org

In article <mk5od.9098$27.1649@newssvr16.news.prodigy.com>,
phlip_cpp@yahoo.com says...
>
>[...]
> > > (And I forgot that Sony's policy is, "we want to make good games, but
> > > not so good that other publishers can't make better ones otherwise
> > > they'll abandon us like they have Nintendo."
> >
> > More nonsense.
>
> I thought Tom worked at Sony. Oh, sorry - I get it. You mean that Sony's
> corporate policy is nonsense. If that's true, I agree.

You're being a retard. Let me spell it out for you. (a) Sony
does not have any such policy. (b) That was a poor attempt
at sarcasm from Tom.


> Game shops don't need more coders capable of transforming matrices all
> night. They might need a few more guys familiar with sound software
> engineering practices.

For the Nth time, the software engineering problems you are
harping on about are non-problems. The primary problems are
production related, NOT software related.



> Apparently, anyone who says "you can write software without the neurotic
> cycle of creating bugs and then fixing them" must be a looney zealot around
> here. What a culture!

Like your more famous loon counterpart you are tilting at
windmills; you're stuck up on a non-issue.


Christer Ericson
Sony Computer Entertainment, Santa Monica

Christer Ericson wrote:

> You're being a retard. Let me spell it out for you. (a) Sony
> does not have any such policy. (b) That was a poor attempt
> at sarcasm from Tom.

Okay. At the risk of pulling this discussion out of the recess playground
level, may I ask what is Sony's general software development methodology?

> > Apparently, anyone who says "you can write software without the neurotic
> > cycle of creating bugs and then fixing them" must be a looney zealot
around
> > here. What a culture!
>
> Like your more famous loon counterpart you are tilting at
> windmills; you're stuck up on a non-issue.

Who is that? And what issue do you think I was discussing?

(Apologies for losing track, there have been several of them so far!)

--
Phlip
http://industrialxp.org/community/bi...UserInterfaces

In article <rKAod.23406$Rf1.5156@newssvr19.news.prodigy.com >,
phlip_cpp@yahoo.com says...
> [...]
> > You're being a retard. Let me spell it out for you. (a) Sony
> > does not have any such policy. (b) That was a poor attempt
> > at sarcasm from Tom.
>
> Okay. At the risk of pulling this discussion out of the recess playground
> level, may I ask what is Sony's general software development methodology?

There is no such thing as "Sony's general software development
methodology".


> > Like your more famous loon counterpart you are tilting at
> > windmills; you're stuck up on a non-issue.
>
> Who is that? And what issue do you think I was discussing?

Don Quixote. You were yet again implying that game developers have
a problem with rampant bug counts and that agile methodologies
(and perhaps XP and TDD in particular) would rectify those
problems.

However, as I'm now repeating for the N^Nth time, the accounts
of rampant bug counts are highly exaggerated. The majority of
game development problems are production issues, NOT software
engineering issues. Why do you have such a hard time getting
this?

In other words, your favorite newfangled software methodology
of the day does nothing to address what are the real problems
that we have in game development.

Thus, you appearing in these newsgroups behaving like the new
messiah has met with the obvious response, and things will
continue that way until you get a clue or go away.


Christer Ericson
Sony Computer Entertainment, Santa Monica

Christer Ericson wrote:

> There is no such thing as "Sony's general software development
> methodology".

Because computers don't receive mental telepathy very well yet, you can't
get software without implementing it. Everyone who writes software follows
some kind of pattern or technique.

> > > Like your more famous loon counterpart you are tilting at
> > > windmills; you're stuck up on a non-issue.
> >
> > Who is that? And what issue do you think I was discussing?
>
> Don Quixote. You were yet again implying that game developers have
> a problem with rampant bug counts and that agile methodologies
> (and perhaps XP and TDD in particular) would rectify those
> problems.

All software has a problem with high bug rates. If game programming doesn't,
then maybe I _do_ need to learn more about what people are doing!

> However, as I'm now repeating for the N^Nth time, the accounts
> of rampant bug counts are highly exaggerated. The majority of
> game development problems are production issues, NOT software
> engineering issues. Why do you have such a hard time getting
> this?

Because I never saw a very large scale project, with multiple Software
Product Lines, and with a long build process, that did not have delays and
process waste caused by debugging. Hey, what can I say? It's a windmill that
looks a _lot_ like a giant!

(Please also keep in mind I'm also reluctant to dish on my employer. Our
loyalty should not be taken as obfuscation.)

> In other words, your favorite newfangled software methodology
> of the day does nothing to address what are the real problems
> that we have in game development.

"Newfangled"? TDD was used for the software on the Gemini missions.

I have heard that Scrum is useful for aligning the developers and the
producers. I don't see how it could hurt.

I have also seen first hand how tuning a build process, and switching
debugging to bug-prevention, can stabilize extraordinarily large projects,
reducing the turnaround time. This can't but help relations with producers.
At one gig, when the linguists generated new content, I could build it, test
it, and wrap it up into an MSI and deliver it within a few minutes. The
build scripts formerly required several days of mucking. These efficiencies
gave producers more freedom in selecting short-term goals; more steering.

I'm not saying that agile techniques will automatically shorten a build
process. I'm saying that as it shortens, producers get feedback from their
own decisions faster. When that feedback is very slow, process waste will
_always_ occur, but it may take many forms.

(You may want to open the book /The Game Asset Pipeline/ by Ben Carter, turn
to page 6, and read the last sentence of the subsection "The Game Asset
Pipeline" for a second opinion here...

--
Phlip
http://industrialxp.org/community/bi...UserInterfaces

On Tue, 23 Nov 2004, Phlip wrote:

> All software has a problem with high bug rates.

Horseshit. Unless, of course, you're going to keep shifting the goals on
what counts as high. Some of us have decent techniques for avoiding bugs
already.

--
flippa@flippac.org

Phlip <phlip_cpp@yahoo.com> loquated like no one had ever loquated before
with:

> Christer Ericson wrote:
>
>> There is no such thing as "Sony's general software development
>> methodology".
>
> Because computers don't receive mental telepathy very well yet, you
> can't get software without implementing it. Everyone who writes
> software follows some kind of pattern or technique.

I usually write of your more stupid responses to pedagogical rhetoric, but
I'm starting to think that you really do not understand what Christer meant
by *** There is no such thing as "Sony's general software development
methodology". ***

You're exhibiting one of two potential problems. Please let us know which
one applies. First, you honestly don't understand that "no such thing as
'Sony's general software development methodology" means there's no establish
corpus of processes for every game development team at Sony. Second, you're
a typical evangelizing zealot who constantly deflects counter-points and
disputations with feigned confusion and/or itentional misinterpretation
(i.e. as above where you ridiculously assume that because there's no GENERAL
software development methodology that there would, de facto, then be no
methodologies used by anyone if there wasn't a 'general' one.)

Which of those two people would you like to be? Stupid, or an ass?
Personally, I think you're just being an ass.

> All software has a problem with high bug rates. If game programming
> doesn't, then maybe I _do_ need to learn more about what people are
> doing!

Maybe you should define high bug rates first, and software second.
Personally, I've worked on several projects with VERY low bug rates;
however, it always seems to follow the philosophy of fast, cheap, good:
Pick any two.

> Because I never saw a very large scale project, with multiple Software
> Product Lines, and with a long build process, that did not have
> delays and process waste caused by debugging. Hey, what can I say?
> It's a windmill that looks a _lot_ like a giant!

What a strawman... You're in the game development ng evangelizing for XP,
and using a non game development example for your pontificating. I wonder
why people (like myself) find you actually detrimental to the adoption of
'agile' methodologies.

> (Please also keep in mind I'm also reluctant to dish on my employer.
> Our loyalty should not be taken as obfuscation.)

Who cares, you have never done any professional game development, why would
'dishing' on your current employer convince people that you know what is
wrong with game development as a whole?

>> In other words, your favorite newfangled software methodology
>> of the day does nothing to address what are the real problems
>> that we have in game development.
>
> "Newfangled"? TDD was used for the software on the Gemini missions.

I'm sorry, is the only thing you're talking about now TDD? I mean, you've
been throwing around the word 'agile' for a while now. Most people who know
anything about XP know that it is generally just a mix of practices from
other methodologies.

> I have also seen first hand how tuning a build process, and switching
> debugging to bug-prevention, can stabilize extraordinarily large
> projects, reducing the turnaround time. This can't but help relations
> with producers. At one gig, when the linguists generated new content,
> I could build it, test it, and wrap it up into an MSI and deliver it
> within a few minutes. The build scripts formerly required several
> days of mucking. These efficiencies gave producers more freedom in
> selecting short-term goals; more steering.

Funny, now 'tuning a build process' only happens when embracing 'agile'
methods. My build process currently (23 projects, roughly 600-700k loc)
takes 0 minutes and 0 seconds to add a foreign language to our product.
Beat that.

> I'm not saying that agile techniques will automatically shorten a
> build process. I'm saying that as it shortens, producers get feedback
> from their own decisions faster. When that feedback is very slow,
> process waste will _always_ occur, but it may take many forms.

This is where the fundamental purpose of XP comes to light. XP is most
valuable as an emergency methodology (although parts of it are useful in any
scenario if they appeal to you), in order to accomodate for shitty
management. XP grew because product managers wouldn't make decisions, sales
personnel were involved beyond the initial spec, because development began
without a decent design, because feature creep became problematics, yadda
yadda yadda. All the problems that arise from everybody and their dog
wanting to make software w/o learning how to do it (on the non-technical
side most importantly.)

> (You may want to open the book /The Game Asset Pipeline/ by Ben
> Carter, turn to page 6, and read the last sentence of the subsection
> "The Game Asset Pipeline" for a second opinion here...

A second opinion which is talking about production issues? Well, now you're
making Christer's points for him.

WTH

Philippa Cowderoy <flippa@flippac.org> loquated like no one had ever
loquated before with:

> On Tue, 23 Nov 2004, Phlip wrote:
>
>> All software has a problem with high bug rates.
>
> Horseshit. Unless, of course, you're going to keep shifting the goals
> on what counts as high. Some of us have decent techniques for
> avoiding bugs already.

Well, surely you must be fully embracing 'agile' methodologies to accomplish
such a wondrous feat...

WTH

Philippa Cowderoy wrote:

> Phlip wrote:
>
> > All software has a problem with high bug rates.
>
> Horseshit. Unless, of course, you're going to keep shifting the goals on
> what counts as high. Some of us have decent techniques for avoiding bugs
> already.

I saw an XP team that had finished a moderately complex visualization tool
for gas chromatographic tools in 6 months once. They had 2 defects on their
board. Teams working like that have the option to never use their debugger.

I am not going to shift any goals on what counts as too high.

--
Phlip
http://industrialxp.org/community/bi...UserInterfaces