Bookmarks [2011/04/27]

  • Groklaw - 1 + 1 (pat. pending) — Mathematics, Software and Free Speech

    tags: freedom, math, software

    This article provides a detailed factual explanation of why software is mathematics, complete with the references in mathematical and computer science literature. It also includes a detailed factual explanation of why mathematics is speech, complete once again with references. My hope is that it will help patent lawyers and judges handling patent litigation understand these fundamental truths, so they can apply that technical knowledge to their field of skill.

  • What is Coq ? | The Coq Proof Assistant

    tags: programming, langugage, math, software

    Coq allows:

    • to define functions or predicates, that can be evaluated efficiently;
    • to state mathematical theorems and software specifications;
    • to interactively develop formal proofs of these theorems;
    • to machine-check these proofs by a relatively small certification "kernel";
    • to extract certified programs to languages like Objective Caml, Haskell or Scheme.
  • Your taste is why your own work disappoints you

    tags: work, advice, insight, howto, hack

    For the first couple years you make stuff, it's just not that good. It's trying to be good, it has potential, but it's not. But your taste, the thing that got you into the game, is still killer. And your taste is why your work disappoints you.

Show comments