# Numbers in Computer Scientist's Eye

The fundation of modern mathmatics is the set theory. If you have gone through some mathmatics course, you would find that every definition comes from set directly or indirectly. For example, one poss

The fundation of modern mathmatics is the set theory. If you have gone through some mathmatics course, you would find that every definition comes from set directly or indirectly. For example, one poss

The problemWhen we try to prove that one general recursion defined in coq is actually correct, in the sense that the fixpoint gives exact the same result if we unfold it once. In words of Coq, it is 1

There is two well-known number representation in computer: one’s complement and two’s complement. While the latter one is widely adopted almost everywhere in the computer, the former one is still used

Summary of last yearIt has been quite a long time since my last post (which is also unfinished). Lots of things has happened and changed since last blog. I’ve been interning at Apple through the end o