What have you found for these years?

2011-07-02

一些想法關於 What Philosophy of Science Can Say for Software Engineers

What Philosophy of Science Can Say for Software Engineers

這篇滿長的,其實我沒很仔細看,有些想法但沒辦法講得很清楚,所以
大概就是隨意摘些文摘吧。邊吃晚餐時邊看的... 雖然這樣可能會消化不良。

Yang 說:

How do we know induction works? We’ve used in the past successfully.
But the act of generalizing this past success to the future is itself
induction, and thus the justification is circular.

這讓我想到之前還沒看完的 Alan Kay 的訪談。
A Conversation with Alan Kay

Kay 提到:

We looked at Java very closely in 1995 when we were starting on a
major set of implementations, just because it’s a lot of work to do a
viable language kernel. The thing we liked least about Java was the
way it was implemented. It had this old idea, which has never worked,
of having a set of paper specs, having to implement the VM (virtual
machine) to the paper specs, and then having benchmarks that try to
validate what you’ve just implemented—and that has never resulted
in a completely compatible system.

用自己來實作自己,稱作 bootstrap, 乍看之下需要多花很多功夫,又不會
有什麼好處。但事實上 Kay 說:

The technique that we had for Smalltalk was to write the VM in itself,
so there’s a Smalltalk simulator of the VM that was essentially the
only specification of the VM. You could debug and you could answer
any question about what the VM would do by submitting stuff to it,
and you made every change that you were going to make to the VM
by changing the simulator. After you had gotten everything debugged
the way you wanted, you pushed the button and it would generate,
without human hands touching it, a mathematically correct version of
C that would go on whatever platform you were trying to get onto.

Java 用 C 去實作的問題是,怎麼確保在不同平台上,所有的實作結果都是
相同的?一個語言可以有兩種方式去定義標準,一個是有個 specification,
然後所有實作要依照這個 spec 去做。怎麼解釋 spec, 誰做的是對的,就看人
解釋了。或是有個 reference implementation, 這個 implementation
怎麼說,那這個 language 的 semantic 就是怎麼樣。

前者我們仰賴人類的解釋,後者則仰賴實作這個語言的語言。以 Java 為例,
就是 C 了。(雖然我不確定 JVM 是不是 C 寫的)然後 C 又仰賴... C.
如果不是 C 呢?

而如果 Smalltalk 實作了 Smalltalk (Squeak), 那改了 Smalltalk VM 整個
Smalltalk 就變了。不管在哪裡的 Smalltalk 都變了。

理論上說來好像合理,但其實我也不是很確定這樣說到底對不對。畢竟我們
當初一定會有一個最早拿來 bootstrap 的 Smalltalk, 到底有沒有算仰賴他?
self-referential 往往會帶來令人困惑的結果..。Gödel's incompleteness
theorems 到現在也還是搞不太懂。

* * *

Yang 說:

Falsification improves over inductivism by embracing the theory-
dependence of observation. Falsificationists don’t care where you
get your theory from, as long as you then attempt to falsify it,
and also accept the fact that there is no way to determine if a
theory is actually true in light of evidence. This latter point is
worth emphasizing: whereas induction attempts to make a
non-deductive step from a few cases to a universal, falsification
can make a deductive step from a negative case to a negative
universal. To use a favorite example, it is logically true that if
there is a white raven, then not all ravens are black. Furthermore,
a theory is better if it is more falsifiable: it suggests a specific set
of tests.

我很喜歡這種說法。有點忘記是在哪裡看到了[0],有人說 test 是程式正確性的
upper bound, 而 proof 則是 lower bound. 解釋起來像是,test 告訴我們
在這些例子中,我們的程式運作是符合預期的。但其實我們真正要的程式的
意義(語意),並沒有那麼多。我們只是窮舉所有可能而已。雖然現實上
其實也沒辦法真的窮舉。另一方面,proof 則是假設這些程式絕對是正確的,
但其實我們要的很可能更多,包括那些沒辦法被證明的!例如 halting problem?

前一陣子,在 twitter 看到有人說這個說法是錯的,但他沒解釋。很想問
為什麼他覺得是錯的... 但也很擔心碰到 test 狂之類的。

很多年前,在 ptt CSSE 上看到「可證偽性」,那時不太明白是什麼意思。
這邊解釋得很清楚。一個愈好的理論,就應該是愈容易可被證明他是錯的。
最簡單的證明就是舉反例就好了。其實這比較像是 test...

也就是說,上述的 inductivism 像是 proof, 而 falsificationism 像是 test.

「可證偽性」應該也是拿來挑戰偽科學很好用的工具之一..。

[0] 我找到了: What To Know Before Debating Type Systems
難怪會說這個說法很有名,這篇本身應該是很有名沒錯..。


這篇應該細讀的,非常有趣。不過這種東西讀多了,就會覺得人類
其實是多麼地不理智,大多理智的思考都是違反直覺的? XD

Yang 說:

Suppose that our crashing program has two bugs (here we use “bug”
in the sense of “source code defect”). Is it true that the first bug
causes the crash? Well, if we removed that bug, the program would
continue to crash. Thus, under the counterfactual theory of causation,
the first bug doesn’t cause the crash. Neither does the second bug,
for that matter. We have a case of causal overdetermination.
(Lewis claims the true cause of the bug is the disjunction of the
two bugs. Perhaps not too surprising for a computer scientist, but
this sounds genuinely weird when applied to every-day life.)

So true. :)

0 retries:

Post a Comment

All texts are licensed under CC Attribution 3.0