$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 2009/04/01

### 兩篇

Science is knowledge which we understand so well that we can teach it to a computer; and if we don’t fully understand something, it is an art to deal with it. (Computer programming as an art)

Many people who pursue formal mathematics are seeking the beauty of complete concreteness, which contributes to their own appreciation of the material being formalised, while to many outside the field formalisation is “just filling in the details” of conventional mathematics. But “just” might be infeasible unless serious thought is given to representation of both the logic of formalisation and the mathematics being formalised. (How to believe a machine-checked proof)

--

Labels: