[cap-talk] Backwater: some small progress

[Mark S. Miller]

Matej Kosik wrote:
> What bothers me on Backwater is that not a science. It is an art or
> engineering. There are many useful statements that are obviously true, for
> example "the ClockMorph has the authority to change 8 characters on the
> screen whose coordinates are: (7,5), (8,5), (9,5), ... , (14,5). If someone
> were able to prove that, that would be a science. I know that it is true
> but I cannot prove it. I do not need the proof in this case very much (the
> truth is so "obvious") but it may be handy if I wanted to persuade others
> about my opinion.


I would say instead, "if someone were able to prove that, then in would be 
math." Indeed, many people (including me) would classify much of the work on 
proving/verifying program correctness as math.

But let's say you indeed continue to fail to prove your conjecture. If your 
conjecture were false -- if the ClockMorph actually has more authority than 
you think it does, then likely someone could disprove your conjecture by 
counter-example. Until then, the absence of a counter-example lends support to 
the plausibility of your conjecture. This sure sounds like science to me.

<http://www.eeng.dcu.ie/~tkpw/> 
<http://www.the-rathouse.com/files/Bartley__1964__limits_of_criticism.doc>
<http://www.the-rathouse.com/bartdogmatic.html>

-- 
Text by me above is hereby placed in the public domain

     Cheers,
     --MarkM