Redian新闻
>
自由工匠弄不了formal verification
avatar
自由工匠弄不了formal verification# Programming - 葵花宝典
w*u
1
NAS用的硬盘有啥特殊要求?西数的绿盘怎么样?谢谢
avatar
W*n
2
绝大部分码农搞的不是critical system,所以可以自由发挥,但最高大上的软件工程
是有严格理论指导的,不是手艺活。
avatar
o*h
3
samsung F4 2T
avatar
g*t
4
每个人都可以选择自己是自由工匠,或者自认为自己是自由工匠。
但是不认自然律,那就是自欺欺人了。没有对规律的认识,哪里来的自由?
avatar
B*G
5
东芝前两天那个50刀2T也不错。
avatar
h*i
6
工匠用一切能实用和适当的工具。需要用formal verifications的地方就用。
你这些条条框框都是什么來的?说说,为什么自由工匠弄不了这个?
avatar
m*d
7
绿盘据据说raid经常出问题
三爽或者deathstar

【在 w**********u 的大作中提到】
: NAS用的硬盘有啥特殊要求?西数的绿盘怎么样?谢谢
avatar
h*i
8
软件有自己的规律,非要套用不适用的物理规律,算什么?


: 每个人都可以选择自己是自由工匠,或者自认为自己是自由工匠。

: 但是不认自然律,那就是自欺欺人了。没有对规律的认识,哪里来的自由?



【在 g****t 的大作中提到】
: 每个人都可以选择自己是自由工匠,或者自认为自己是自由工匠。
: 但是不认自然律,那就是自欺欺人了。没有对规律的认识,哪里来的自由?

avatar
w*u
9
谢楼上几位,怎么发包子?
NAS不用raid 0会很慢吗?
avatar
g*t
10
Computer science有自然律不假。
要不然,怎么可能我说量纲和类型是类似的代数系统,正巧就好多人研究。这必然是同
一个客观的东西被不同的人感觉到才会发生的问题。
你说的三个人做软件属于not even wrong的rant。


: 软件有自己的规律,非要套用不适用的物理规律,算什么?



【在 h*i 的大作中提到】
: 软件有自己的规律,非要套用不适用的物理规律,算什么?
:
:
: 每个人都可以选择自己是自由工匠,或者自认为自己是自由工匠。
:
: 但是不认自然律,那就是自欺欺人了。没有对规律的认识,哪里来的自由?
:

avatar
w*u
11
新蛋那个吗?不是$60AR吗

【在 B*G 的大作中提到】
: 东芝前两天那个50刀2T也不错。
avatar
g*t
12
第一,我讲的是非常严谨的。开始我讲了not claim正确。
第二,我看到有人做,有产品上来才当作论据的。
第三,物理学的算术计算,不用算数规律用什么。同理,物理计算牵涉到computer
science的当然是用计算机科学的规律。


: 软件有自己的规律,非要套用不适用的物理规律,算什么?



【在 h*i 的大作中提到】
: 软件有自己的规律,非要套用不适用的物理规律,算什么?
:
:
: 每个人都可以选择自己是自由工匠,或者自认为自己是自由工匠。
:
: 但是不认自然律,那就是自欺欺人了。没有对规律的认识,哪里来的自由?
:

avatar
m*d
13
用了那个10off新用户吧,或者15off50的新用户coupon
不过新蛋运硬盘doa率太高,总是很烦

【在 w**********u 的大作中提到】
: 新蛋那个吗?不是$60AR吗
avatar
h*i
14
写软件这个手艺的一个基本功是能读懂CS文献和具有对文章实用性的判断力,然后就是
能实现和提高文献算法的能力。没这点本事的是不能算会这门手艺的。
Clojure 社区里稍微有点名的人物几乎个个都是如此吧。
avatar
w*u
15
新开了个newegg账户,49.99AR买了东芝那个,谢谢
avatar
p*o
16
说到formal verification, Lamport搞TLA+算自由工匠么?

【在 W*********n 的大作中提到】
: 绝大部分码农搞的不是critical system,所以可以自由发挥,但最高大上的软件工程
: 是有严格理论指导的,不是手艺活。

avatar
m*d
17
日历吧?现在还有东芝硬盘吗?

【在 w**********u 的大作中提到】
: 新开了个newegg账户,49.99AR买了东芝那个,谢谢
avatar
h*i
18
软件的规律和数学是不同的。你的问题就是把这二者等价化。马尔的分层理论对你来说
是不是很陌生?reductionism 听说过没?


: Computer science有自然律不假。

: 要不然,怎么可能我说量纲和类型是类似的代数系统,正巧就好多人研究。这必
然是同

: 一个客观的东西被不同的人感觉到才会发生的问题。

: 你说的三个人做软件属于not even wrong的rant。



【在 g****t 的大作中提到】
: 第一,我讲的是非常严谨的。开始我讲了not claim正确。
: 第二,我看到有人做,有产品上来才当作论据的。
: 第三,物理学的算术计算,不用算数规律用什么。同理,物理计算牵涉到computer
: science的当然是用计算机科学的规律。
:
:
: 软件有自己的规律,非要套用不适用的物理规律,算什么?
:

avatar
N*S
19
nas 就别用raid0了,瓶颈应该是网络传输速度。
avatar
h*i
20
我说的软件二人律是一个软件科学范畴内的一个hypotheses,你认为是rant,可见对软
件科学的对象是什么都不知道。鸡同鸭讲。


: Computer science有自然律不假。

: 要不然,怎么可能我说量纲和类型是类似的代数系统,正巧就好多人研究。这必
然是同

: 一个客观的东西被不同的人感觉到才会发生的问题。

: 你说的三个人做软件属于not even wrong的rant。



【在 g****t 的大作中提到】
: 第一,我讲的是非常严谨的。开始我讲了not claim正确。
: 第二,我看到有人做,有产品上来才当作论据的。
: 第三,物理学的算术计算,不用算数规律用什么。同理,物理计算牵涉到computer
: science的当然是用计算机科学的规律。
:
:
: 软件有自己的规律,非要套用不适用的物理规律,算什么?
:

avatar
g*t
21
我之前自己发展的量纲分析和type theory的类比,不是给了专家的工作,以及hack
news的评论。不算computer science ? 你觉得你更懂type theory, 自己开心就行。别
拿buzz word吓唬我。


: 软件的规律和数学是不同的。你的问题就是把这二者等价化。马尔的分层
理论对
你来说

: 是不是很陌生?reductionism 听说过没?

: 然是同



【在 h*i 的大作中提到】
: 我说的软件二人律是一个软件科学范畴内的一个hypotheses,你认为是rant,可见对软
: 件科学的对象是什么都不知道。鸡同鸭讲。
:
:
: Computer science有自然律不假。
:
: 要不然,怎么可能我说量纲和类型是类似的代数系统,正巧就好多人研究。这必
: 然是同
:
: 一个客观的东西被不同的人感觉到才会发生的问题。
:
: 你说的三个人做软件属于not even wrong的rant。
:

avatar
h*i
22
认了就好。科学计算是一个很狭窄的专门领域,CS都不太算,软件就更远了,你还是少
评论一些不懂的东西。


: 我之前自己发展的量纲分析和type theory的类比,不是给了专家的工作,以及
hack

: news的评论。不算computer science ? 你觉得你更懂type theory, 自己开心就
行。别

: 拿buzz word吓唬我。

:

【在 g****t 的大作中提到】
: 我之前自己发展的量纲分析和type theory的类比,不是给了专家的工作,以及hack
: news的评论。不算computer science ? 你觉得你更懂type theory, 自己开心就行。别
: 拿buzz word吓唬我。
:
:
: 软件的规律和数学是不同的。你的问题就是把这二者等价化。马尔的分层
: 理论对
: 你来说
:
: 是不是很陌生?reductionism 听说过没?
:
: 然是同
:

avatar
g*t
23
软件是engineering, computer science是科学。
我只是觉得没必要帮你的 软件二人论 不停打patch。举个例子你就说不是软件。
事实上,就算是计算机系的传统项目,质量好点的数据库,OS 进程scheduler, GC,编
译器...都包含很多不同CS细节分支的知识。现在那都不是两个人能做的软件。
你认为软件二人论是科学。那么good luck。
我在讨论中,独立提出type theory和量纲系统的类比,这是别的专家也认可的较新的
问题。
所以我对这个收
获没啥不满意的。也对你表示感谢。


: 认了就好。科学计算是一个很狭窄的专门领域,CS都不太算,软件就更远
了,你
还是少

: 评论一些不懂的东西。

: hack

: 行。别



【在 h*i 的大作中提到】
: 认了就好。科学计算是一个很狭窄的专门领域,CS都不太算,软件就更远了,你还是少
: 评论一些不懂的东西。
:
:
: 我之前自己发展的量纲分析和type theory的类比,不是给了专家的工作,以及
: hack
:
: news的评论。不算computer science ? 你觉得你更懂type theory, 自己开心就
: 行。别
:
: 拿buzz word吓唬我。
:
:

avatar
h*i
24
我就把话挑明了说,type theory对软件工程几乎没有任何用处。
你说这些那些都不是两个人能做的,那应该很容易举例啊。结果一个例子都没有。我这
个conjecture still stands. 我也很想看看有没有什么反例,可就是没有啊。

【在 g****t 的大作中提到】
: 软件是engineering, computer science是科学。
: 我只是觉得没必要帮你的 软件二人论 不停打patch。举个例子你就说不是软件。
: 事实上,就算是计算机系的传统项目,质量好点的数据库,OS 进程scheduler, GC,编
: 译器...都包含很多不同CS细节分支的知识。现在那都不是两个人能做的软件。
: 你认为软件二人论是科学。那么good luck。
: 我在讨论中,独立提出type theory和量纲系统的类比,这是别的专家也认可的较新的
: 问题。
: 所以我对这个收
: 获没啥不满意的。也对你表示感谢。
:

avatar
h*c
25
james gosling 去了亚马逊,
一个语言被广泛的应用后,和原作者没有啥关系了,比如长城第一个设计出来砖块的工
匠,觉得黄金分割的比例更好些,但长城修到了雁门关,和你没有任何关系了。
以前讲过说sun有一款机器不停的莫名其妙当机,gosling以前博客写的,现在找不到了
,有人怀疑是宇宙射线,因为好像是费米试验室报告的这个问题,后来发现是一个CPU
供应商的供货辐射超标。
我觉得偏离对计算机器最基础的理解,工程对于可靠性要求的理解,夸夸棋坛。没有什
么意义。
动态类型,非常拉稀。是一种辐射超标的CPU。是一种drama.
avatar
h*c
26
实际最近这些很多框架根本没有严格设计施工监理和验收,比如谷歌的GWT,后来的
angular,可以说这些互联网公司本来就没有设计过什么好的软件。
所谓的搜索,就是图书馆学的索引理论。大数据也是基于存储技术提供的可靠性。
多数连个spec都拿不出来,就要银行医院,发电站飞机场来用,就是诈骗
avatar
g*t
27
这点你说的是对的。过去这些年mobile时代造成互联网流量爆炸性增加。跑马圈地为主
,系统先上线边走边修,属于多阶段优化过程。
Android最开始我拿到一个现在已经倒闭的公司的手机。稍加操作就会死机,重启的。
还卖的非常贵。但是最后的结果是人家一点点修好了。


: 实际最近这些很多框架根本没有严格设计施工监理和验收,比如谷歌的GWT,后
来的

: angular,可以说这些互联网公司本来就没有设计过什么好的软件。

: 所谓的搜索,就是图书馆学的索引理论。大数据也是基于存储技术提供的可靠性。

: 多数连个spec都拿不出来,就要银行医院,发电站飞机场来用,就是诈骗



【在 h**********c 的大作中提到】
: 实际最近这些很多框架根本没有严格设计施工监理和验收,比如谷歌的GWT,后来的
: angular,可以说这些互联网公司本来就没有设计过什么好的软件。
: 所谓的搜索,就是图书馆学的索引理论。大数据也是基于存储技术提供的可靠性。
: 多数连个spec都拿不出来,就要银行医院,发电站飞机场来用,就是诈骗

avatar
h*i
28
这就是我说的,软件的特殊性。用搞硬件的思维来看软件,那简直就是一团糟,太不严
谨了,
因为写软件其实与写书更接近,好的书,名作,masterpiece,是一两个人写的。但也
有文集,还有谬传了千年的故事集,流传最广的反而是后者。比如摆布书,就是被千百
人在千百年中篡改了多次的故事集,但没人说摆布书是一个masterpiece。其实这些都
是正常人都理解的东西,没有必要争辩这些。
我说的东西,唯一新的信息,就是写软件与写文章类似。

性。

【在 g****t 的大作中提到】
: 这点你说的是对的。过去这些年mobile时代造成互联网流量爆炸性增加。跑马圈地为主
: ,系统先上线边走边修,属于多阶段优化过程。
: Android最开始我拿到一个现在已经倒闭的公司的手机。稍加操作就会死机,重启的。
: 还卖的非常贵。但是最后的结果是人家一点点修好了。
:
:
: 实际最近这些很多框架根本没有严格设计施工监理和验收,比如谷歌的GWT,后
: 来的
:
: angular,可以说这些互联网公司本来就没有设计过什么好的软件。
:
: 所谓的搜索,就是图书馆学的索引理论。大数据也是基于存储技术提供的可靠性。
:
: 多数连个spec都拿不出来,就要银行医院,发电站飞机场来用,就是诈骗

avatar
R*e
29
formalverification可用的地方太少了,经常是npc以上的复杂度。不反对用,只要效
率高就行。

【在 W*********n 的大作中提到】
: 绝大部分码农搞的不是critical system,所以可以自由发挥,但最高大上的软件工程
: 是有严格理论指导的,不是手艺活。

avatar
x*u
30
人脑靠的是动态规划,找出大概没问题的解,所以软件bug无数
将来早晚彻底换成神经网络,省去编码这个步骤

【在 R******e 的大作中提到】
: formalverification可用的地方太少了,经常是npc以上的复杂度。不反对用,只要效
: 率高就行。

avatar
R*e
31
AM模型或者概率证明模型得出:np难问题是不可近似的,所以神经网络作为一种组合电
路,即使得出np问题的近似解,也不大可能很又瘦又浅。

【在 x****u 的大作中提到】
: 人脑靠的是动态规划,找出大概没问题的解,所以软件bug无数
: 将来早晚彻底换成神经网络,省去编码这个步骤

avatar
x*u
32
足够用即可
用GPS寻路也是NP,但照样瞬间给你大概率找到最短路线
假如np问题可以近似,那人类就不是人类,而是全知全能的上帝了

【在 R******e 的大作中提到】
: AM模型或者概率证明模型得出:np难问题是不可近似的,所以神经网络作为一种组合电
: 路,即使得出np问题的近似解,也不大可能很又瘦又浅。

avatar
h*c
33
动态类型金腰带,形式验证无尸骸
相关阅读
logo
联系我们隐私协议©2024 redian.news
Redian新闻
Redian.news刊载任何文章,不代表同意其说法或描述,仅为提供更多信息,也不构成任何建议。文章信息的合法性及真实性由其作者负责,与Redian.news及其运营公司无关。欢迎投稿,如发现稿件侵权,或作者不愿在本网发表文章,请版权拥有者通知本网处理。