
tags: howto
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.
cdixon.org – chris dixon’s blog / There are two kinds of people in the world
tags: life, startup, advice, people
The important distinction is whether you risked everything, put your life on the line, made commitments to investors, employees, customers and friends, and tried – against all the forces in the world that try to keep new ideas down – to make something new.
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 machinecheck 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.