Re: What databases have taught me

Tony D wrote:
> topmind wrote:
> > Tony D wrote:
> > > Ye gods. I'll limit my response to that to a comment on the metrics.
> > > How about "correctness" ?
> >
> > Yes, but as pointed out in the link, there are multiple paths to the
> > same "answer". Nobody is defending something that produces the wrong
> > answer here.
> >
>
> But how do you *know* you've got the "same 'answer'" ?
>
> > > Or, "provability" ?
> >
> > Very few are attempting to use formal proofs to prove their software
> > correct. It has generally been easier to have 3 teams write different
> > code based on the same specs and then have the system use majority
> > rules if one is off.
> >
>
> I'm sorry, my brain just fell out of my ear at that suggestion. You're
> really telling me you'd get three teams to write software to the same
> spec then take the majority vote as a proof of correctness ? I suppose
> it proves the old saw about there never being time to do it right, but
> always time to do it over. And over.

I am just saying that formal software proving has proved (pun) tedious and slow so far.

>
> > > Or, "ability to reason
> > > about what this software actually does,
> >
> > This is rather subjective, though.
>
> I don't think it is; you can either formally reason about what your
> code does, or you can't. There are some concepts regularly bandied
> about in programming languages that don't have a formal underpinning,
> so you're at the mercy of the "definition" of whatever language you're
> using. And even then, the ultimate arbiter is the implementation you're
> using, whatever the language "spec" says. (And if the language spec is
> ambiguous, or insufficiently precise or formal, two compilers, or even
> two optimiser levels in the same compiler, can produce different
> outputs and still be "right". What hope then ?)

Can you provide an example? It is not clear to me what you are proposing.

>
> > I've encountered people who could
> > reason about Goto's far better than I could. Somebody will invariably
> > say, "If you were smart like me, you could reason about my code." I
> > guarentee it.
> >
>
> Yes, and people used to write code that took advantage of the
> rotational delay of drum memory to avoid coding jumps. That was pretty
> damn stupid too. There will always be some smartass-cum-guru kicking
> around pulling that kind of crazy stunt. Safest thing to do with them
> is to kick them out, or conscript them to the Department of Special
> (and Irrelevant) Projects. Anything to limit the chaos they can leave
> in their wake (generally, about a week after they leave/retire/fall
> under a bus).

Back then the drum probably cost more than the programmer. Scraping for every last bit mattered back then. Only in the early 70's did software maintanence and management become more important than hardware.

>
> > > without resorting to stuffing
> > > some more-or-less random test cases through it as some kind of
> > > demonstration that it kind-of, maybe, perhaps does what we want it to,
> > > for these semi-random test cases at least ?"
> >
> > I have kicked around approaches to measure the code impact of various
> > change scenarios. The problem is that people also perceive change
> > differently, I've found out, such that they would assign different
> > frequency estimates, which were required to get a total score.
> >
>
> Exactly. You've "kicked around approaches to measure the code impact of
> various change scenarios". But without being able to formally reason
> about behaviour in the abstract, before a piece of code is even
> written, you're fighting a losing battle, making more-or-less educated
> guesses.

Again, it is not clear to me what you are proposing. Formal proving is not a common industry practice.

-T- Received on Sun Jul 09 2006 - 05:45:04 CEST