g*t
2 楼
物理定律的量綱和諧性，簡而言之，也就是說對任何數字，方程左右邊的單位必須一
致。這個東西表面上看起來很簡單和顯然。實際上非常powerful。
我感覺量綱驗證和程序裡變量的數據類型的正確性驗證是類似的。（量綱分析有時候還
可以告訴我们，你的系統需要的自由參數的lower bound。这点和机器学习其实是有关
系的。如果一種fitting出來的模型，其量綱不對，則必然錯誤。）
总之，我觉得計算機語言的类型系统第一作用是：find bug sooner
反過來看。計算語言類型系統為什麼仍然沒辦法dominate?
我覺得原因在於，現有的類型演算的模型不太對，沒有一種例如可以叫做typed Turing
machine的方便的模型。
致。這個東西表面上看起來很簡單和顯然。實際上非常powerful。
我感覺量綱驗證和程序裡變量的數據類型的正確性驗證是類似的。（量綱分析有時候還
可以告訴我们，你的系統需要的自由參數的lower bound。这点和机器学习其实是有关
系的。如果一種fitting出來的模型，其量綱不對，則必然錯誤。）
总之，我觉得計算機語言的类型系统第一作用是：find bug sooner
反過來看。計算語言類型系統為什麼仍然沒辦法dominate?
我覺得原因在於，現有的類型演算的模型不太對，沒有一種例如可以叫做typed Turing
machine的方便的模型。
e*6
3 楼
见光绿
j*w
4 楼
> 我觉得計算機語言的类型系统第一作用是：find bug sooner
某种程度你是对的。
编程语言的类型系统有两个主要的作用：
1 尽早发现 bugs。类型系统可以在编译时发现一些类型相关的 bugs - 这些 bugs 进
入 debug 和 production 的阶段时，修复成本成数量级增加。Note: 类型推导（即无
需程序员标注类型）仍然维系类型系统；
2 提高运行时性能，包括时间和空间。在运算符计算之前，参与计算的变量的类型必须
确定。要么是编译时确定，要么是运行时确定。没有免费的午餐。
类似 C 的静态类型语言，变量的类型在编译的时候就确定，所以在编译的时候就能生
成确定的机器指令，在运行时无需再考量变量的类型。像 Lua 这样的动态类型语言，
编译时变量的类型无法确定，那么这个工作只能够放到运行时来做。所以 Lua 的每一
个值里面都有一个域保存该变量的类型，在运行时 vm 会检查。这样的话运行速度会慢
好多。
某种程度你是对的。
编程语言的类型系统有两个主要的作用：
1 尽早发现 bugs。类型系统可以在编译时发现一些类型相关的 bugs - 这些 bugs 进
入 debug 和 production 的阶段时，修复成本成数量级增加。Note: 类型推导（即无
需程序员标注类型）仍然维系类型系统；
2 提高运行时性能，包括时间和空间。在运算符计算之前，参与计算的变量的类型必须
确定。要么是编译时确定，要么是运行时确定。没有免费的午餐。
类似 C 的静态类型语言，变量的类型在编译的时候就确定，所以在编译的时候就能生
成确定的机器指令，在运行时无需再考量变量的类型。像 Lua 这样的动态类型语言，
编译时变量的类型无法确定，那么这个工作只能够放到运行时来做。所以 Lua 的每一
个值里面都有一个域保存该变量的类型，在运行时 vm 会检查。这样的话运行速度会慢
好多。
h*h
5 楼
谢谢。
绿了以后，能放在冰箱里吗？
【在 e*****6 的大作中提到】
: 见光绿
绿了以后，能放在冰箱里吗？
【在 e*****6 的大作中提到】
: 见光绿
j*w
6 楼
> 計算語言類型系統為什麼仍然沒辦法dominate?
这只是程序语言设计时做的一个 tradeoff 而已。看语言设计者在设计的时候面向的使
用场景是什么。
你在语法中引入显式的类型，好处是提升运行时性能，但是会增加程序员的认知负担。
把类型从语法中抹掉，好处是减少程序员认知负担，但是可能会削弱运行时性能。
假如你设计的语言主要用于简单脚本或者嵌入，那么没必要引入重量的类型系统，比如
Perl, Python, Lua, JavaScript, Ruby 等。
但是如果你的语言是系统级的语言，用来开发几千万 LOC 的系统的话，那么需要一个
类型系统。
哪怕同一种语言也是可以变的。同样一种语言，当它应用场景变复杂的时候会加上类型
系统，比如：
JavaScript -> TypeScript，微软
PHP -> Hack，Facebook
Python -> Python with type annotation
用途是多样的，所以没有必要 dominate。
这只是程序语言设计时做的一个 tradeoff 而已。看语言设计者在设计的时候面向的使
用场景是什么。
你在语法中引入显式的类型，好处是提升运行时性能，但是会增加程序员的认知负担。
把类型从语法中抹掉，好处是减少程序员认知负担，但是可能会削弱运行时性能。
假如你设计的语言主要用于简单脚本或者嵌入，那么没必要引入重量的类型系统，比如
Perl, Python, Lua, JavaScript, Ruby 等。
但是如果你的语言是系统级的语言，用来开发几千万 LOC 的系统的话，那么需要一个
类型系统。
哪怕同一种语言也是可以变的。同样一种语言，当它应用场景变复杂的时候会加上类型
系统，比如：
JavaScript -> TypeScript，微软
PHP -> Hack，Facebook
Python -> Python with type annotation
用途是多样的，所以没有必要 dominate。
d*g
7 楼
能的
【在 h*h 的大作中提到】
: 谢谢。
: 绿了以后，能放在冰箱里吗？
【在 h*h 的大作中提到】
: 谢谢。
: 绿了以后，能放在冰箱里吗？
g*t
8 楼
决定语言的速度的第一因素是看它是编译的，还是解释的。
而不是看它有没有类型。
无类型语言也可以很快。例如編譯型的Lisp，它有很快的版本。
:
【在 j*****w 的大作中提到】
: > 計算語言類型系統為什麼仍然沒辦法dominate?
: 这只是程序语言设计时做的一个 tradeoff 而已。看语言设计者在设计的时候面向的使
: 用场景是什么。
: 你在语法中引入显式的类型，好处是提升运行时性能，但是会增加程序员的认知负担。
: 把类型从语法中抹掉，好处是减少程序员认知负担，但是可能会削弱运行时性能。
: 假如你设计的语言主要用于简单脚本或者嵌入，那么没必要引入重量的类型系统，比如
: Perl, Python, Lua, JavaScript, Ruby 等。
: 但是如果你的语言是系统级的语言，用来开发几千万 LOC 的系统的话，那么需要一个
: 类型系统。
: 哪怕同一种语言也是可以变的。同样一种语言，当它应用场景变复杂的时候会加上类型
而不是看它有没有类型。
无类型语言也可以很快。例如編譯型的Lisp，它有很快的版本。
:
【在 j*****w 的大作中提到】
: > 計算語言類型系統為什麼仍然沒辦法dominate?
: 这只是程序语言设计时做的一个 tradeoff 而已。看语言设计者在设计的时候面向的使
: 用场景是什么。
: 你在语法中引入显式的类型，好处是提升运行时性能，但是会增加程序员的认知负担。
: 把类型从语法中抹掉，好处是减少程序员认知负担，但是可能会削弱运行时性能。
: 假如你设计的语言主要用于简单脚本或者嵌入，那么没必要引入重量的类型系统，比如
: Perl, Python, Lua, JavaScript, Ruby 等。
: 但是如果你的语言是系统级的语言，用来开发几千万 LOC 的系统的话，那么需要一个
: 类型系统。
: 哪怕同一种语言也是可以变的。同样一种语言，当它应用场景变复杂的时候会加上类型
q*r
9 楼
半个多月，早就过了绿的时间了吧。 绿就是几天而已啊。
【在 h*h 的大作中提到】
: 是美国的苹果醋，在冰箱里泡了半个多月了。也许温度太低？今天把它拿出来看会不会
: 几天后变绿。
【在 h*h 的大作中提到】
: 是美国的苹果醋，在冰箱里泡了半个多月了。也许温度太低？今天把它拿出来看会不会
: 几天后变绿。
j*w
10 楼
编译的代码当然比解释的代码运行更快。
但是我说的是，一个在编译时无法完全推导类型的语言哪怕在编译成二进制代码后，仍
然会比同等条件下静态类型语言的速度要慢。为什么？
当看到 a + b 的时候，如果编译器无法确定 a 或者 b 的类型，但是又需要编译成机
器语言的话，你想应该怎么办？只能是把所有的类型组合的代码都编译进去。比如 int
+ int, int + string, string + int, ...，并且在前面加上类型判断分支。
那么运行的时候，每次需要把两个变量相加的时候，都需要执行额外的分支代码，速度
自然就慢了。
这是 Google 做的工作：
https://pdfs.semanticscholar.org/a77b/72481ddf51c45495d64bf3335871183e0e4c.
pdf
【在 g****t 的大作中提到】
: 决定语言的速度的第一因素是看它是编译的，还是解释的。
: 而不是看它有没有类型。
: 无类型语言也可以很快。例如編譯型的Lisp，它有很快的版本。
:
:
:
但是我说的是，一个在编译时无法完全推导类型的语言哪怕在编译成二进制代码后，仍
然会比同等条件下静态类型语言的速度要慢。为什么？
当看到 a + b 的时候，如果编译器无法确定 a 或者 b 的类型，但是又需要编译成机
器语言的话，你想应该怎么办？只能是把所有的类型组合的代码都编译进去。比如 int
+ int, int + string, string + int, ...，并且在前面加上类型判断分支。
那么运行的时候，每次需要把两个变量相加的时候，都需要执行额外的分支代码，速度
自然就慢了。
这是 Google 做的工作：
https://pdfs.semanticscholar.org/a77b/72481ddf51c45495d64bf3335871183e0e4c.
【在 g****t 的大作中提到】
: 决定语言的速度的第一因素是看它是编译的，还是解释的。
: 而不是看它有没有类型。
: 无类型语言也可以很快。例如編譯型的Lisp，它有很快的版本。
:
:
:
e*6
11 楼
很奇怪，
你搞的蒜是想绿，绿不了
我腌的蒜想不绿，却绿了
绿了以后应该可以放冰箱的吧，
我以前腌过一次，就是剥了皮，直接存冰箱的，
绿得很，头一次看见那么绿的蒜，
以为是坏的，就一狠心把一瓶香喷喷的腊八蒜给扔了
【在 h*h 的大作中提到】
: 谢谢。
: 绿了以后，能放在冰箱里吗？
你搞的蒜是想绿，绿不了
我腌的蒜想不绿，却绿了
绿了以后应该可以放冰箱的吧，
我以前腌过一次，就是剥了皮，直接存冰箱的，
绿得很，头一次看见那么绿的蒜，
以为是坏的，就一狠心把一瓶香喷喷的腊八蒜给扔了
【在 h*h 的大作中提到】
: 谢谢。
: 绿了以后，能放在冰箱里吗？
g*t
12 楼
倒内存也可以加速的。例如整数全当double处理。在预处理代码阶段，每个整数都乘以
1.0
int
【在 j*****w 的大作中提到】
: 编译的代码当然比解释的代码运行更快。
: 但是我说的是，一个在编译时无法完全推导类型的语言哪怕在编译成二进制代码后，仍
: 然会比同等条件下静态类型语言的速度要慢。为什么？
: 当看到 a + b 的时候，如果编译器无法确定 a 或者 b 的类型，但是又需要编译成机
: 器语言的话，你想应该怎么办？只能是把所有的类型组合的代码都编译进去。比如 int
: + int, int + string, string + int, ...，并且在前面加上类型判断分支。
: 那么运行的时候，每次需要把两个变量相加的时候，都需要执行额外的分支代码，速度
: 自然就慢了。
: 这是 Google 做的工作：
: https://pdfs.semanticscholar.org/a77b/72481ddf51c45495d64bf3335871183e0e4c.
1.0
int
【在 j*****w 的大作中提到】
: 编译的代码当然比解释的代码运行更快。
: 但是我说的是，一个在编译时无法完全推导类型的语言哪怕在编译成二进制代码后，仍
: 然会比同等条件下静态类型语言的速度要慢。为什么？
: 当看到 a + b 的时候，如果编译器无法确定 a 或者 b 的类型，但是又需要编译成机
: 器语言的话，你想应该怎么办？只能是把所有的类型组合的代码都编译进去。比如 int
: + int, int + string, string + int, ...，并且在前面加上类型判断分支。
: 那么运行的时候，每次需要把两个变量相加的时候，都需要执行额外的分支代码，速度
: 自然就慢了。
: 这是 Google 做的工作：
: https://pdfs.semanticscholar.org/a77b/72481ddf51c45495d64bf3335871183e0e4c.
h*i
13 楼
Simple fact: what a type system can prove is too weak and too little.
Yes, people can attempt to prove more and more, but it will NEVER be
sufficient.
There's hard limit on the applicability of mathematical logic on human
problems. In the end, there's Gödel's incompleteness theorems.
Realizing the limitation of logics for understanding human cognition,
certain genius was totally devastated. e.g. Walter Pitts, the guy who made
genius like John von Neumann looked like dumb, and was solving Norbert
Wiener's problems without any efforts.
https://en.wikipedia.org/wiki/Walter_Pitts
You are nowhere comparable with these guys. Don't waste your time.
Turing
【在 g****t 的大作中提到】
: 物理定律的量綱和諧性，簡而言之，也就是說對任何數字，方程左右邊的單位必須一
: 致。這個東西表面上看起來很簡單和顯然。實際上非常powerful。
: 我感覺量綱驗證和程序裡變量的數據類型的正確性驗證是類似的。（量綱分析有時候還
: 可以告訴我们，你的系統需要的自由參數的lower bound。这点和机器学习其实是有关
: 系的。如果一種fitting出來的模型，其量綱不對，則必然錯誤。）
: 总之，我觉得計算機語言的类型系统第一作用是：find bug sooner
: 反過來看。計算語言類型系統為什麼仍然沒辦法dominate?
: 我覺得原因在於，現有的類型演算的模型不太對，沒有一種例如可以叫做typed Turing
: machine的方便的模型。
Yes, people can attempt to prove more and more, but it will NEVER be
sufficient.
There's hard limit on the applicability of mathematical logic on human
problems. In the end, there's Gödel's incompleteness theorems.
Realizing the limitation of logics for understanding human cognition,
certain genius was totally devastated. e.g. Walter Pitts, the guy who made
genius like John von Neumann looked like dumb, and was solving Norbert
Wiener's problems without any efforts.
https://en.wikipedia.org/wiki/Walter_Pitts
You are nowhere comparable with these guys. Don't waste your time.
Turing
【在 g****t 的大作中提到】
: 物理定律的量綱和諧性，簡而言之，也就是說對任何數字，方程左右邊的單位必須一
: 致。這個東西表面上看起來很簡單和顯然。實際上非常powerful。
: 我感覺量綱驗證和程序裡變量的數據類型的正確性驗證是類似的。（量綱分析有時候還
: 可以告訴我们，你的系統需要的自由參數的lower bound。这点和机器学习其实是有关
: 系的。如果一種fitting出來的模型，其量綱不對，則必然錯誤。）
: 总之，我觉得計算機語言的类型系统第一作用是：find bug sooner
: 反過來看。計算語言類型系統為什麼仍然沒辦法dominate?
: 我覺得原因在於，現有的類型演算的模型不太對，沒有一種例如可以叫做typed Turing
: machine的方便的模型。
g*t
14 楼
In near future, there is no way to remove the units/type system
from physics/chemistry and computer science. Live with it or keep ranting,
it is just a choice that did not have relationship with natural laws or
moral laws.
【在 h*i 的大作中提到】
: Simple fact: what a type system can prove is too weak and too little.
: Yes, people can attempt to prove more and more, but it will NEVER be
: sufficient.
: There's hard limit on the applicability of mathematical logic on human
: problems. In the end, there's Gödel's incompleteness theorems.
: Realizing the limitation of logics for understanding human cognition,
: certain genius was totally devastated. e.g. Walter Pitts, the guy who made
: genius like John von Neumann looked like dumb, and was solving Norbert
: Wiener's problems without any efforts.
: https://en.wikipedia.org/wiki/Walter_Pitts
from physics/chemistry and computer science. Live with it or keep ranting,
it is just a choice that did not have relationship with natural laws or
moral laws.
【在 h*i 的大作中提到】
: Simple fact: what a type system can prove is too weak and too little.
: Yes, people can attempt to prove more and more, but it will NEVER be
: sufficient.
: There's hard limit on the applicability of mathematical logic on human
: problems. In the end, there's Gödel's incompleteness theorems.
: Realizing the limitation of logics for understanding human cognition,
: certain genius was totally devastated. e.g. Walter Pitts, the guy who made
: genius like John von Neumann looked like dumb, and was solving Norbert
: Wiener's problems without any efforts.
: https://en.wikipedia.org/wiki/Walter_Pitts
a*e
15 楼
Type is an intrinsic property of a program, regardless of whether a
programmer realizes it or not, whether it is declared or derived, whether it
is checked at compile or run time.
这和发现 bug 或者提高性能没有任何关系。
在类型系统层面上的编程已经很成熟了，和各种逻辑系统的关系紧密。
programmer realizes it or not, whether it is declared or derived, whether it
is checked at compile or run time.
这和发现 bug 或者提高性能没有任何关系。
在类型系统层面上的编程已经很成熟了，和各种逻辑系统的关系紧密。
h*i
16 楼
You didn't seem to understand that the type system of computing has nothing
to do with unit/dimension of physical systems.
unit/dimension of physical systems need to be explicitly represented as data
in computers, which is precisely what Clojure people advocate, i.e. {:kg
1000 :color :red}.
The automatic typing people in computer science is not doing that. They
imagine that they can do away with explicit encoding of such information and
derive everything. Keep dreaming.
【在 g****t 的大作中提到】
: In near future, there is no way to remove the units/type system
: from physics/chemistry and computer science. Live with it or keep ranting,
: it is just a choice that did not have relationship with natural laws or
: moral laws.
to do with unit/dimension of physical systems.
unit/dimension of physical systems need to be explicitly represented as data
in computers, which is precisely what Clojure people advocate, i.e. {:kg
1000 :color :red}.
The automatic typing people in computer science is not doing that. They
imagine that they can do away with explicit encoding of such information and
derive everything. Keep dreaming.
【在 g****t 的大作中提到】
: In near future, there is no way to remove the units/type system
: from physics/chemistry and computer science. Live with it or keep ranting,
: it is just a choice that did not have relationship with natural laws or
: moral laws.
g*t
17 楼
First,I felt that the type system and dimensional analysis in physics
had close relationship. At that time, I said that I did not claim I was
correct since I did not went into the details.
Then,last night, I found that quit a few experts had the same feelings. One
expert had developed a theory and applied in the F sharp. (see links I gave
previously)
nothing
data
and
【在 h*i 的大作中提到】
: You didn't seem to understand that the type system of computing has nothing
: to do with unit/dimension of physical systems.
: unit/dimension of physical systems need to be explicitly represented as data
: in computers, which is precisely what Clojure people advocate, i.e. {:kg
: 1000 :color :red}.
: The automatic typing people in computer science is not doing that. They
: imagine that they can do away with explicit encoding of such information and
: derive everything. Keep dreaming.
had close relationship. At that time, I said that I did not claim I was
correct since I did not went into the details.
Then,last night, I found that quit a few experts had the same feelings. One
expert had developed a theory and applied in the F sharp. (see links I gave
previously)
nothing
data
and
【在 h*i 的大作中提到】
: You didn't seem to understand that the type system of computing has nothing
: to do with unit/dimension of physical systems.
: unit/dimension of physical systems need to be explicitly represented as data
: in computers, which is precisely what Clojure people advocate, i.e. {:kg
: 1000 :color :red}.
: The automatic typing people in computer science is not doing that. They
: imagine that they can do away with explicit encoding of such information and
: derive everything. Keep dreaming.
h*i
18 楼
These are the "proof people" RH talk about. They are chasing an illusion
that is bound to fail.
These people get resources to try their dream because the dream is shared by
capitalist that want to turn programming into assembly line work.
They will keep failing.
One
gave
【在 g****t 的大作中提到】
: First,I felt that the type system and dimensional analysis in physics
: had close relationship. At that time, I said that I did not claim I was
: correct since I did not went into the details.
: Then,last night, I found that quit a few experts had the same feelings. One
: expert had developed a theory and applied in the F sharp. (see links I gave
: previously)
:
: nothing
: data
: and
that is bound to fail.
These people get resources to try their dream because the dream is shared by
capitalist that want to turn programming into assembly line work.
They will keep failing.
One
gave
【在 g****t 的大作中提到】
: First,I felt that the type system and dimensional analysis in physics
: had close relationship. At that time, I said that I did not claim I was
: correct since I did not went into the details.
: Then,last night, I found that quit a few experts had the same feelings. One
: expert had developed a theory and applied in the F sharp. (see links I gave
: previously)
:
: nothing
: data
: and
g*t
19 楼
It would be better to check if RH understand the challenges of putting
physics Unit calculation into software without using type/class etc. The
answer most likely be a NO.
IMHO
(1)
The power of the type system had been proved in physics.
(2)
Thus, without involving the very specific computers hardware facts, it was
not possible to prove the advantage of non-type programming languages.
Because you need something to separate the physics out of your claims.
In other words, I did not believe that the question of type/no-type
can be answered by a Generic theory. Assuming such a Generic theory is
equivalent to assuming the advantage of No-Units physics.
In a summary, any general claims about the advantage of type(or no type)
need to take care of the power of physics (pure number theory).
by
【在 h*i 的大作中提到】
: These are the "proof people" RH talk about. They are chasing an illusion
: that is bound to fail.
: These people get resources to try their dream because the dream is shared by
: capitalist that want to turn programming into assembly line work.
: They will keep failing.
:
: One
: gave
physics Unit calculation into software without using type/class etc. The
answer most likely be a NO.
IMHO
(1)
The power of the type system had been proved in physics.
(2)
Thus, without involving the very specific computers hardware facts, it was
not possible to prove the advantage of non-type programming languages.
Because you need something to separate the physics out of your claims.
In other words, I did not believe that the question of type/no-type
can be answered by a Generic theory. Assuming such a Generic theory is
equivalent to assuming the advantage of No-Units physics.
In a summary, any general claims about the advantage of type(or no type)
need to take care of the power of physics (pure number theory).
by
【在 h*i 的大作中提到】
: These are the "proof people" RH talk about. They are chasing an illusion
: that is bound to fail.
: These people get resources to try their dream because the dream is shared by
: capitalist that want to turn programming into assembly line work.
: They will keep failing.
:
: One
: gave
h*i
20 楼
Any physics theory can be implemented by computers, but not all computer
programs correspond to physics, i.e.
the virtual world in a computer can be larger than physical world, e.g. you
can have no gravity in your virtual world, but in physical world, you cannot
escape gravity.
This simple fact is what every normal person on the street understand, but
the brain fucked theory people somehow choose not to understand.
【在 g****t 的大作中提到】
: It would be better to check if RH understand the challenges of putting
: physics Unit calculation into software without using type/class etc. The
: answer most likely be a NO.
: IMHO
: (1)
: The power of the type system had been proved in physics.
: (2)
: Thus, without involving the very specific computers hardware facts, it was
: not possible to prove the advantage of non-type programming languages.
: Because you need something to separate the physics out of your claims.
programs correspond to physics, i.e.
the virtual world in a computer can be larger than physical world, e.g. you
can have no gravity in your virtual world, but in physical world, you cannot
escape gravity.
This simple fact is what every normal person on the street understand, but
the brain fucked theory people somehow choose not to understand.
【在 g****t 的大作中提到】
: It would be better to check if RH understand the challenges of putting
: physics Unit calculation into software without using type/class etc. The
: answer most likely be a NO.
: IMHO
: (1)
: The power of the type system had been proved in physics.
: (2)
: Thus, without involving the very specific computers hardware facts, it was
: not possible to prove the advantage of non-type programming languages.
: Because you need something to separate the physics out of your claims.
h*i
21 楼
You don't need type to implement physics. All you needs are symbols. Symbols
without type works fine. If you have not seen it, you should try a LISP.
Seriously, your lack of understanding of basic computer science is
disturbing. How do you think types are represented in computer? As fucking
symbols.
【在 g****t 的大作中提到】
: It would be better to check if RH understand the challenges of putting
: physics Unit calculation into software without using type/class etc. The
: answer most likely be a NO.
: IMHO
: (1)
: The power of the type system had been proved in physics.
: (2)
: Thus, without involving the very specific computers hardware facts, it was
: not possible to prove the advantage of non-type programming languages.
: Because you need something to separate the physics out of your claims.
without type works fine. If you have not seen it, you should try a LISP.
Seriously, your lack of understanding of basic computer science is
disturbing. How do you think types are represented in computer? As fucking
symbols.
【在 g****t 的大作中提到】
: It would be better to check if RH understand the challenges of putting
: physics Unit calculation into software without using type/class etc. The
: answer most likely be a NO.
: IMHO
: (1)
: The power of the type system had been proved in physics.
: (2)
: Thus, without involving the very specific computers hardware facts, it was
: not possible to prove the advantage of non-type programming languages.
: Because you need something to separate the physics out of your claims.
g*t
22 楼
你已经看到我这几天闲聊时候发展出来的时候物理单位和type 的类比是type theory领
域专家在做的方向了。
这种情况下，对我的computer science的基础知识进行质疑有意义吗。
我讲话都是有实战根据。以前我用Mathcad做过计算，这就是我经验过的带有物理单位
演算
，但是没有常见的数据类型的系统。我辛辛苦苦写的给芯片里传感器校准的Mathcad程
序，一直都在以前的公司网站上给买家用。
: You don't need type to implement physics. All you needs are
symbols.
Symbols
: without type works fine. If you have not seen it, you should
try a
LISP.
: Seriously, your lack of understanding of basic computer science
is
: disturbing. How do you think types are represented in computer?
As
fucking
: symbols.
【在 h*i 的大作中提到】
: You don't need type to implement physics. All you needs are symbols. Symbols
: without type works fine. If you have not seen it, you should try a LISP.
: Seriously, your lack of understanding of basic computer science is
: disturbing. How do you think types are represented in computer? As fucking
: symbols.
域专家在做的方向了。
这种情况下，对我的computer science的基础知识进行质疑有意义吗。
我讲话都是有实战根据。以前我用Mathcad做过计算，这就是我经验过的带有物理单位
演算
，但是没有常见的数据类型的系统。我辛辛苦苦写的给芯片里传感器校准的Mathcad程
序，一直都在以前的公司网站上给买家用。
: You don't need type to implement physics. All you needs are
symbols.
Symbols
: without type works fine. If you have not seen it, you should
try a
LISP.
: Seriously, your lack of understanding of basic computer science
is
: disturbing. How do you think types are represented in computer?
As
fucking
: symbols.
【在 h*i 的大作中提到】
: You don't need type to implement physics. All you needs are symbols. Symbols
: without type works fine. If you have not seen it, you should try a LISP.
: Seriously, your lack of understanding of basic computer science is
: disturbing. How do you think types are represented in computer? As fucking
: symbols.
h*i
23 楼
你说的和做过的事情是一致的，就是你是个科学计算的domain expert，不是一个职业
搞软件的人。软件工程是一个你没有任何经验的domain，你不要搞混了。
: 你已经看到我这几天闲聊时候发展出来的时候物理单位和type 的类比是type
theory领
: 域专家在做的方向了。
: 这种情况下，对我的computer science的基础知识进行质疑有意义吗。
: 我讲话都是有实战根据。以前我用Mathcad做过计算，这就是我经验过的带有物
理单位
: 演算
: ，但是没有常见的数据类型的系统。我辛辛苦苦写的给芯片里传感器校准的
Mathcad程
: 序，一直都在以前的公司网站上给买家用。
:
【在 g****t 的大作中提到】
: 你已经看到我这几天闲聊时候发展出来的时候物理单位和type 的类比是type theory领
: 域专家在做的方向了。
: 这种情况下，对我的computer science的基础知识进行质疑有意义吗。
: 我讲话都是有实战根据。以前我用Mathcad做过计算，这就是我经验过的带有物理单位
: 演算
: ，但是没有常见的数据类型的系统。我辛辛苦苦写的给芯片里传感器校准的Mathcad程
: 序，一直都在以前的公司网站上给买家用。
:
:
: You don't need type to implement physics. All you needs are
: symbols.
搞软件的人。软件工程是一个你没有任何经验的domain，你不要搞混了。
: 你已经看到我这几天闲聊时候发展出来的时候物理单位和type 的类比是type
theory领
: 域专家在做的方向了。
: 这种情况下，对我的computer science的基础知识进行质疑有意义吗。
: 我讲话都是有实战根据。以前我用Mathcad做过计算，这就是我经验过的带有物
理单位
: 演算
: ，但是没有常见的数据类型的系统。我辛辛苦苦写的给芯片里传感器校准的
Mathcad程
: 序，一直都在以前的公司网站上给买家用。
:
【在 g****t 的大作中提到】
: 你已经看到我这几天闲聊时候发展出来的时候物理单位和type 的类比是type theory领
: 域专家在做的方向了。
: 这种情况下，对我的computer science的基础知识进行质疑有意义吗。
: 我讲话都是有实战根据。以前我用Mathcad做过计算，这就是我经验过的带有物理单位
: 演算
: ，但是没有常见的数据类型的系统。我辛辛苦苦写的给芯片里传感器校准的Mathcad程
: 序，一直都在以前的公司网站上给买家用。
:
:
: You don't need type to implement physics. All you needs are
: symbols.
g*t
24 楼
都是卖的。凭啥科学计算软件不是软件工程。搞混的是你才对。
再说你一個堅持 軟件二人論 的，好意思講我沒有經驗。十八年前我就在幾百人的組做
過後
端。你給說一下，类似上海市公交地铁一卡通这样的项目，三個人能做吗？如何做？三个
人的话，读卡器部分都写不完。很多卡在當初雜亂無章，都有domain knowledge,不是
寫個界面就可以外包出去那麼簡單。
: 你说的和做过的事情是一致的，就是你是个科学计算的domain expert，
不是一
个职业
: 搞软件的人。软件工程是一个你没有任何经验的domain，你不要搞混了。
: theory领
: 理单位
: Mathcad程
【在 h*i 的大作中提到】
: 你说的和做过的事情是一致的，就是你是个科学计算的domain expert，不是一个职业
: 搞软件的人。软件工程是一个你没有任何经验的domain，你不要搞混了。
:
:
: 你已经看到我这几天闲聊时候发展出来的时候物理单位和type 的类比是type
: theory领
:
: 域专家在做的方向了。
:
: 这种情况下，对我的computer science的基础知识进行质疑有意义吗。
:
: 我讲话都是有实战根据。以前我用Mathcad做过计算，这就是我经验过的带有物
: 理单位
:
: 演算
再说你一個堅持 軟件二人論 的，好意思講我沒有經驗。十八年前我就在幾百人的組做
過後
端。你給說一下，类似上海市公交地铁一卡通这样的项目，三個人能做吗？如何做？三个
人的话，读卡器部分都写不完。很多卡在當初雜亂無章，都有domain knowledge,不是
寫個界面就可以外包出去那麼簡單。
: 你说的和做过的事情是一致的，就是你是个科学计算的domain expert，
不是一
个职业
: 搞软件的人。软件工程是一个你没有任何经验的domain，你不要搞混了。
: theory领
: 理单位
: Mathcad程
【在 h*i 的大作中提到】
: 你说的和做过的事情是一致的，就是你是个科学计算的domain expert，不是一个职业
: 搞软件的人。软件工程是一个你没有任何经验的domain，你不要搞混了。
:
:
: 你已经看到我这几天闲聊时候发展出来的时候物理单位和type 的类比是type
: theory领
:
: 域专家在做的方向了。
:
: 这种情况下，对我的computer science的基础知识进行质疑有意义吗。
:
: 我讲话都是有实战根据。以前我用Mathcad做过计算，这就是我经验过的带有物
: 理单位
:
: 演算
h*i
25 楼
当然科学计算不算软件工程。科学计算往往都是一个软件的模块而已，不是一个独立的
软件。你那个卖的东西，肯定也是这样。
你说的例子，和二人律不矛盾。
1. domain knowledge需要很多人，和我说的写软件就两人，没有任何矛盾。
2. 大型项目，分块往往是明显的，必然是分组分头做自己的软件。每个组的软件的写
作，也是符合二人律的。
三个
【在 g****t 的大作中提到】
: 都是卖的。凭啥科学计算软件不是软件工程。搞混的是你才对。
: 再说你一個堅持 軟件二人論 的，好意思講我沒有經驗。十八年前我就在幾百人的組做
: 過後
: 端。你給說一下，类似上海市公交地铁一卡通这样的项目，三個人能做吗？如何做？三个
: 人的话，读卡器部分都写不完。很多卡在當初雜亂無章，都有domain knowledge,不是
: 寫個界面就可以外包出去那麼簡單。
:
:
: 你说的和做过的事情是一致的，就是你是个科学计算的domain expert，
: 不是一
: 个职业
软件。你那个卖的东西，肯定也是这样。
你说的例子，和二人律不矛盾。
1. domain knowledge需要很多人，和我说的写软件就两人，没有任何矛盾。
2. 大型项目，分块往往是明显的，必然是分组分头做自己的软件。每个组的软件的写
作，也是符合二人律的。
三个
【在 g****t 的大作中提到】
: 都是卖的。凭啥科学计算软件不是软件工程。搞混的是你才对。
: 再说你一個堅持 軟件二人論 的，好意思講我沒有經驗。十八年前我就在幾百人的組做
: 過後
: 端。你給說一下，类似上海市公交地铁一卡通这样的项目，三個人能做吗？如何做？三个
: 人的话，读卡器部分都写不完。很多卡在當初雜亂無章，都有domain knowledge,不是
: 寫個界面就可以外包出去那麼簡單。
:
:
: 你说的和做过的事情是一致的，就是你是个科学计算的domain expert，
: 不是一
: 个职业
相关阅读
node.js用http实现websocket,真是神了。Tensorflow course (FREE Deep Learning)继续掐12306老姜来看三亚到三亚的火车票有大牛用最浅显易懂的方式解释一下vert.x到底是什么东西么？网站上的航班信息获取 (转载)哪种跨平台编辑器能把文字和代码都比较好的组合水太大了，谁给个摘要吧考考大家，其实也不只是C++，C#/Java也一样为啥 c++ bit operation的优先级这么低"short" in Java怎么读javascript？go 的坑（转载）请问怎样打开一个有密码的Access数据库 (转载)JAVA 考试题请教share a aws account技术揭秘12306改造：尖峰日PV值297亿下可每秒出票1032张请推荐ios应用开发教程？ (转载)TeacherWei 的订票机的问题12306这个能做成一个轮子吗？