d****i
发帖数: 4809 | 1 随手拿个mathoverflow上的帖子，你们能看的懂吗?
http://mathoverflow.net/questions/196148/non-separable-banach-s
“不可分割的巴拿赫空间”。这个才是人家搞数学的真正关心的东西，这里吹嘘fp的有
几个可以看懂？ |
l*******e
发帖数: 309 | 2 最早的计算机科学家如John von Neumann，Alan Turing就是数学家。现在搞
theoretical computer science的人也是数学家。
FP比OOP更接近数学没错。 |
d****i
发帖数: 4809 | 3 再深入一点可以看看人家关于搞数论的张益唐教授理论证明的讨论，这些才是真正的数学
http://mathoverflow.net/questions/131185/philosophy-behind-yita
【在 d****i 的大作中提到】
: 随手拿个mathoverflow上的帖子，你们能看的懂吗?
: http://mathoverflow.net/questions/196148/non-separable-banach-s
: “不可分割的巴拿赫空间”。这个才是人家搞数学的真正关心的东西，这里吹嘘fp的有
: 几个可以看懂？
|
l*********s
发帖数: 5409 | 4 逻辑有问题啊。你没巴菲特有钱，二爷也没巴菲特有钱，所以你们两个一样都是穷鬼？
数学
【在 d****i 的大作中提到】
: 再深入一点可以看看人家关于搞数论的张益唐教授理论证明的讨论，这些才是真正的数学
: http://mathoverflow.net/questions/131185/philosophy-behind-yita
|
z****e
发帖数: 54598 | 5 fp为了伺候机器
不准用变量，不准用复杂的数据结构
这算哪门子数学？
数学什么时候是以伺候机器为目的而存在的了？
没有变量就没有方程，没有方程的数学是什么数学？
几何？代数？还是分析？难道是统计？
这玩意能算是理科不？哪个phd做点啥研究不放点变量进去？ |
l*******e
发帖数: 309 | 6 FP哪门子数学: Category theory / Type theory
伺候机器: 哪里伺候机器了，正相反把？以前不流行就是因为没有好的Compiler伺候好
机器.现在GHC很厉害了。 |
z****e
发帖数: 54598 | 7 那你说说fp用了变量会有什么副作用
type theory是cs自己发明出来的东西吧
logic就喜欢扯这种蛋
【在 l*******e 的大作中提到】
: FP哪门子数学: Category theory / Type theory
: 伺候机器: 哪里伺候机器了，正相反把？以前不流行就是因为没有好的Compiler伺候好
: 机器.现在GHC很厉害了。
|
l**********n
发帖数: 8443 | 8 The hardware implementation of almost all computers is imperative. |
z****e
发帖数: 54598 | 9 函数式编程的三大特性：
immutable data 不可变数据：像Clojure一样，默认上变量是不可变的，如果你要改变
变量，你需要把变量copy出去修改。这样一来，可以让你的程序少很多Bug。因为，程
序中的状态不好维护，在并发的时候更不好维护。（你可以试想一下如果你的程序有个
复杂的状态，当以后别人改你代码的时候，是很容易出bug的，在并行中这样的问题就
更多了）
说白了就是你用变量容易出问题，状态变来变去，会导致多线程之间的各种问题
但是因此干掉状态，强迫你不用变量，那又是另外一回事
不用变量的数学也能叫数学？我觉得应该叫哲学，文科生比较适合
而且多线程的状态并发等问题，也有其他很多方法予以解决
不应该坚持immutable |
d****i
发帖数: 4809 | 10 你说的有道理，非但type theory是CS自己发明出来的，连fp的所谓的理论基石lambda
calculus都被真正的数学家所不屑，而且被数学家证明理论上是错的。这玩意人家搞数
学的根本不鸟。搞数学的根本不关心什么程序语言，只要一张纸一支笔就可以了。
【在 z****e 的大作中提到】
: 那你说说fp用了变量会有什么副作用
: type theory是cs自己发明出来的东西吧
: logic就喜欢扯这种蛋
|
|
|
l******t
发帖数: 55733 | 11 zkss
lambda
【在 d****i 的大作中提到】
: 你说的有道理，非但type theory是CS自己发明出来的，连fp的所谓的理论基石lambda
: calculus都被真正的数学家所不屑，而且被数学家证明理论上是错的。这玩意人家搞数
: 学的根本不鸟。搞数学的根本不关心什么程序语言，只要一张纸一支笔就可以了。
|
a*****e
发帖数: 1700 | 12 我劝你不懂不要装懂。你倒是点个名道个姓，说说都有哪些“真正的数学家”不屑
lambda calculus 了？数学领域这么广，一个数学家，对自己领域外的东西不了解不研
究很正常，但要说“不屑”或者“抨击”，请给出处。还“证明理论上是错的”？你做
梦呢吧？
而且 type theory 虽然是 CS 的发明，但它和 logic 的对应关系可不是“发明”，而
是 discovery，而且是多次 re-discovery。
lambda
【在 d****i 的大作中提到】
: 你说的有道理，非但type theory是CS自己发明出来的，连fp的所谓的理论基石lambda
: calculus都被真正的数学家所不屑，而且被数学家证明理论上是错的。这玩意人家搞数
: 学的根本不鸟。搞数学的根本不关心什么程序语言，只要一张纸一支笔就可以了。
|
d****i
发帖数: 4809 | 13 不要一击中你的G点就high, 什么时候FP能造出个操作系统出来，或者做点更有用实际
的，把水变成油，把泥土做成蛋糕，把臭水沟变成清水河，把人送上火星再来忽悠。
【在 a*****e 的大作中提到】
: 我劝你不懂不要装懂。你倒是点个名道个姓，说说都有哪些“真正的数学家”不屑
: lambda calculus 了？数学领域这么广，一个数学家，对自己领域外的东西不了解不研
: 究很正常，但要说“不屑”或者“抨击”，请给出处。还“证明理论上是错的”？你做
: 梦呢吧？
: 而且 type theory 虽然是 CS 的发明，但它和 logic 的对应关系可不是“发明”，而
: 是 discovery，而且是多次 re-discovery。
:
: lambda
|
a*****e
发帖数: 1700 | 14 能回答就回答，不能回答就老实承认自己在 troll。
FP 写的操作系统 L4，从头到脚 formally verified： http://sel4.systems
FP 写的 Unikernel, OS, Driver, Lib, App 一整套直接编译成 VM image 可以 boot
： http://www.openmirage.org 这伙人是搞 Xen Hypervisor 的。
【在 d****i 的大作中提到】
: 不要一击中你的G点就high, 什么时候FP能造出个操作系统出来，或者做点更有用实际
: 的，把水变成油，把泥土做成蛋糕，把臭水沟变成清水河，把人送上火星再来忽悠。
|
d****i
发帖数: 4809 | 15 还从头倒脚，一眼过去分明都是C的代码。你学究气和fp宗教味太重，和你道不同，我
只喜欢能够真正解决实际问题的东西，所有主流语言都做到了。不相信fp这种虚无飘渺
忽悠牛角尖的东西。有这时间我还不如去学法语和西班牙语。
boot
【在 a*****e 的大作中提到】
: 能回答就回答，不能回答就老实承认自己在 troll。
: FP 写的操作系统 L4，从头到脚 formally verified： http://sel4.systems
: FP 写的 Unikernel, OS, Driver, Lib, App 一整套直接编译成 VM image 可以 boot
: ： http://www.openmirage.org 这伙人是搞 Xen Hypervisor 的。
|
j********x
发帖数: 2330 | 16 lz你会画结构结构图么？
这都不会
谈nmb的架构啊？。。。
【在 d****i 的大作中提到】
: 随手拿个mathoverflow上的帖子，你们能看的懂吗?
: http://mathoverflow.net/questions/196148/non-separable-banach-s
: “不可分割的巴拿赫空间”。这个才是人家搞数学的真正关心的东西，这里吹嘘fp的有
: 几个可以看懂？
|
d****i
发帖数: 4809 | 17 你画个你妈逼的结构图给我看看，要不画个你的菊花逼图也可。
【在 j********x 的大作中提到】
: lz你会画结构结构图么？
: 这都不会
: 谈nmb的架构啊？。。。
|
a*****e
发帖数: 1700 | 18 你眼神不好，看的 seL4 的 github 吗？看见这句话了？
"haskell: Haskell model of the seL4 kernel, kept in sync with the C version."
缺了这个，根本没办法做 formal verification。想明白怎么回事就去读一下人家的论
文吧。
【在 d****i 的大作中提到】
: 还从头倒脚，一眼过去分明都是C的代码。你学究气和fp宗教味太重，和你道不同，我
: 只喜欢能够真正解决实际问题的东西，所有主流语言都做到了。不相信fp这种虚无飘渺
: 忽悠牛角尖的东西。有这时间我还不如去学法语和西班牙语。
:
: boot
|
a*****e
发帖数: 1700 | 19 看你这么不愿意接触自己不懂的东西，我给你截个图好了，整个系统只有一块是 C，其
它都是 FP 系的。而且我说的是“从头到脚 formally verified”，什么意思呢？
We then describe the functional correctness proof of the kernel’s C
implementation and we cover further steps that transform this result into a
comprehensive formal verification of the kernel: a formally verified IPC
fast path, a proof that the binary code of the kernel correctly implements
the C semantics, a proof of correct access-control enforcement, a proof of
information-flow noninterference, a sound worst-case execution time analysis
of the binary, and an automatic initialiser for user-level systems that
connects kernel-level access control enforcement with reasoning about system
behaviour.
【在 d****i 的大作中提到】
: 还从头倒脚，一眼过去分明都是C的代码。你学究气和fp宗教味太重，和你道不同，我
: 只喜欢能够真正解决实际问题的东西，所有主流语言都做到了。不相信fp这种虚无飘渺
: 忽悠牛角尖的东西。有这时间我还不如去学法语和西班牙语。
:
: boot
|
j********x
发帖数: 2330 | 20 nonono
你听我说
楼主tmb的是个傻逼
你不要跟着他起哄
【在 d****i 的大作中提到】
: 你画个你妈逼的结构图给我看看，要不画个你的菊花逼图也可。
|
z****e
发帖数: 54598 | 21 马甲你越来越blaze化了
【在 j********x 的大作中提到】
: nonono
: 你听我说
: 楼主tmb的是个傻逼
: 你不要跟着他起哄
|
j********x
发帖数: 2330 | 22 blaze说我是你马甲
你又说我是马甲
是不是可以打脸blaze这傻吊了。。。
【在 z****e 的大作中提到】
: 马甲你越来越blaze化了
|
