整天拿fp来说事的看看人家真正的数学家的东东 - 未名空间MITBBS历史存档

国际科技财经博客移民网络热点娱乐民生时事公众号

Redian新闻

>未名空间

>Programming - 葵花宝典

整天拿fp来说事的看看人家真正的数学家的东东

整天拿fp来说事的看看人家真正的数学家的东东# Programming - 葵花宝典

s*m2015-02-12 08:02

1 楼

刚新开了一个ATT family plan
data plan也已经有了
手机不是iphone4 开plan时候送的android的智能手机
想搞台没有绑定数据plan的iphone4
店里面有的要卖599+tax
不知道这里有人知道哪能买到比较便宜的裸机iphone4吗？
谢谢啦！

d*i2015-02-12 08:02

2 楼

随手拿个mathoverflow上的帖子，你们能看的懂吗?
http://mathoverflow.net/questions/196148/non-separable-banach-s
“不可分割的巴拿赫空间”。这个才是人家搞数学的真正关心的东西，这里吹嘘fp的有
几个可以看懂？

d*y2015-02-12 08:02

3 楼

craigslish....
电话公司会查你的手机是不是smart phone的
如果系统查出来自动给你加上data plan

l*e2015-02-12 08:02

4 楼

最早的计算机科学家如John von Neumann，Alan Turing就是数学家。现在搞
theoretical computer science的人也是数学家。
FP比OOP更接近数学没错。

s*m2015-02-12 08:02

5 楼

我已经有data plan了

【在 d*******y 的大作中提到】

: craigslish....
: 电话公司会查你的手机是不是smart phone的
: 如果系统查出来自动给你加上data plan

d*i2015-02-12 08:02

6 楼

再深入一点可以看看人家关于搞数论的张益唐教授理论证明的讨论，这些才是真正的数学
http://mathoverflow.net/questions/131185/philosophy-behind-yita

【在 d****i 的大作中提到】

: 随手拿个mathoverflow上的帖子，你们能看的懂吗?
: http://mathoverflow.net/questions/196148/non-separable-banach-s
: “不可分割的巴拿赫空间”。这个才是人家搞数学的真正关心的东西，这里吹嘘fp的有
: 几个可以看懂？

l*s2015-02-12 08:02

7 楼

逻辑有问题啊。你没巴菲特有钱，二爷也没巴菲特有钱，所以你们两个一样都是穷鬼？

数学

【在 d****i 的大作中提到】

: 再深入一点可以看看人家关于搞数论的张益唐教授理论证明的讨论，这些才是真正的数学
: http://mathoverflow.net/questions/131185/philosophy-behind-yita

z*e2015-02-12 08:02

8 楼

fp为了伺候机器
不准用变量，不准用复杂的数据结构
这算哪门子数学？
数学什么时候是以伺候机器为目的而存在的了？
没有变量就没有方程，没有方程的数学是什么数学？
几何？代数？还是分析？难道是统计？
这玩意能算是理科不？哪个phd做点啥研究不放点变量进去？

l*e2015-02-12 08:02

9 楼

FP哪门子数学: Category theory / Type theory
伺候机器: 哪里伺候机器了，正相反把？以前不流行就是因为没有好的Compiler伺候好
机器.现在GHC很厉害了。

z*e2015-02-12 08:02

10 楼

那你说说fp用了变量会有什么副作用
type theory是cs自己发明出来的东西吧
logic就喜欢扯这种蛋

【在 l*******e 的大作中提到】

: FP哪门子数学: Category theory / Type theory
: 伺候机器: 哪里伺候机器了，正相反把？以前不流行就是因为没有好的Compiler伺候好
: 机器.现在GHC很厉害了。

l*n2015-02-12 08:02

11 楼

The hardware implementation of almost all computers is imperative.

z*e2015-02-12 08:02

12 楼

函数式编程的三大特性：
immutable data 不可变数据：像Clojure一样，默认上变量是不可变的，如果你要改变
变量，你需要把变量copy出去修改。这样一来，可以让你的程序少很多Bug。因为，程
序中的状态不好维护，在并发的时候更不好维护。（你可以试想一下如果你的程序有个
复杂的状态，当以后别人改你代码的时候，是很容易出bug的，在并行中这样的问题就
更多了）
说白了就是你用变量容易出问题，状态变来变去，会导致多线程之间的各种问题
但是因此干掉状态，强迫你不用变量，那又是另外一回事
不用变量的数学也能叫数学？我觉得应该叫哲学，文科生比较适合
而且多线程的状态并发等问题，也有其他很多方法予以解决
不应该坚持immutable

d*i2015-02-12 08:02

13 楼

你说的有道理，非但type theory是CS自己发明出来的，连fp的所谓的理论基石lambda
calculus都被真正的数学家所不屑，而且被数学家证明理论上是错的。这玩意人家搞数
学的根本不鸟。搞数学的根本不关心什么程序语言，只要一张纸一支笔就可以了。

【在 z****e 的大作中提到】

: 那你说说fp用了变量会有什么副作用
: type theory是cs自己发明出来的东西吧
: logic就喜欢扯这种蛋

l*t2015-02-12 08:02

14 楼

zkss

lambda

【在 d****i 的大作中提到】

: 你说的有道理，非但type theory是CS自己发明出来的，连fp的所谓的理论基石lambda
: calculus都被真正的数学家所不屑，而且被数学家证明理论上是错的。这玩意人家搞数
: 学的根本不鸟。搞数学的根本不关心什么程序语言，只要一张纸一支笔就可以了。

a*e2015-02-12 08:02

15 楼

我劝你不懂不要装懂。你倒是点个名道个姓，说说都有哪些“真正的数学家”不屑
lambda calculus 了？数学领域这么广，一个数学家，对自己领域外的东西不了解不研
究很正常，但要说“不屑”或者“抨击”，请给出处。还“证明理论上是错的”？你做
梦呢吧？
而且 type theory 虽然是 CS 的发明，但它和 logic 的对应关系可不是“发明”，而
是 discovery，而且是多次 re-discovery。

lambda

【在 d****i 的大作中提到】

d*i2015-02-12 08:02

16 楼

不要一击中你的G点就high, 什么时候FP能造出个操作系统出来，或者做点更有用实际
的，把水变成油，把泥土做成蛋糕，把臭水沟变成清水河，把人送上火星再来忽悠。

【在 a*****e 的大作中提到】

: 我劝你不懂不要装懂。你倒是点个名道个姓，说说都有哪些“真正的数学家”不屑
: lambda calculus 了？数学领域这么广，一个数学家，对自己领域外的东西不了解不研
: 究很正常，但要说“不屑”或者“抨击”，请给出处。还“证明理论上是错的”？你做
: 梦呢吧？
: 而且 type theory 虽然是 CS 的发明，但它和 logic 的对应关系可不是“发明”，而
: 是 discovery，而且是多次 re-discovery。
:
: lambda

a*e2015-02-12 08:02

17 楼

能回答就回答，不能回答就老实承认自己在 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*i2015-02-12 08:02

18 楼

还从头倒脚，一眼过去分明都是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*x2015-02-12 08:02

19 楼

lz你会画结构结构图么？
这都不会
谈nmb的架构啊？。。。

【在 d****i 的大作中提到】

d*i2015-02-12 08:02

20 楼

你画个你妈逼的结构图给我看看，要不画个你的菊花逼图也可。

【在 j********x 的大作中提到】

: lz你会画结构结构图么？
: 这都不会
: 谈nmb的架构啊？。。。

a*e2015-02-12 08:02

21 楼

你眼神不好，看的 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*e2015-02-12 08:02

22 楼

看你这么不愿意接触自己不懂的东西，我给你截个图好了，整个系统只有一块是 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 的大作中提到】

j*x2015-02-12 08:02

23 楼

nonono
你听我说
楼主tmb的是个傻逼
你不要跟着他起哄

【在 d****i 的大作中提到】

: 你画个你妈逼的结构图给我看看，要不画个你的菊花逼图也可。

z*e2015-02-12 08:02

24 楼

马甲你越来越blaze化了

【在 j********x 的大作中提到】

: nonono
: 你听我说
: 楼主tmb的是个傻逼
: 你不要跟着他起哄

j*x2015-02-12 08:02

25 楼

blaze说我是你马甲
你又说我是马甲
是不是可以打脸blaze这傻吊了。。。

【在 z****e 的大作中提到】

: 马甲你越来越blaze化了