I think the general program of categorical logic, the work of Lambek and Scott, and J. Bell on topos theory and local set theory really make clear the relationship between category theory and logic, as well as lambda calculus.
A topos is essentially a cartesian closed category with a subject classifier. In Set this is the two element set of 1/0 which is a Boolean algebra and thus the internal logic of the category Set is classical.
In general though the subobject classifier is a heyting algebra which expresses the semantics of intuitionistic logic.
There is also a very good, but introductory, book by Goldblatt on Topoi that covers this logical aspect
So in terms of logics the category of Sets is the exception.
By internal logic I mean that for every topos one builds up a theory using it's objects and function between them. An equivalence theorem (see J. Bell) states that a given topos is essentially equal to the category generated by this internal theory.
This program began with Lawvere who noticed that conjunction and implication were really adjoints, the same one as between the product and hom functors in a cartesian closed category.
> Of course a problem was that in 1984 the modern importance of free software wasn't really apparent.
Perhaps it wasn't apparent widely, but it was certainly clear to MSFT and IBM. IBM lawyers at the time refused to allow RMS to come speak at the Watson lab where I worked, because of his ideas about free software.
According to Bloomberg, margin requirements are going to be quite high in order to keep bitcoin trading from creating issues.
If you can trade bitcoin futures in Chicago, to me that says regulation is coming, and even central bank involvement. Seems to go against the grain of what bitcoin pretends to be about.
#2. Exactly, seems to me an academic kind of thing, he helped them a lot, a little attribution would not have hurt, and the lawyers could have easily been told to pipe down.
#3. It does offer the maximum freedom to some potential users, but no responsibilities to extend those freedoms to others. In my opinion this is why the GPL truly extends the maximum amount of freedom to everyone, users, lusers, abusers, and just plain old hackers.
One of the best papers I've read on cartesian duality was by Vaughan Pratt[1] on Chu spaces. It's a little bit of a slog for those not conversant in foundations, but it does help ground the conversation in terms that are more rigorous.
As an aside, Chu spaces also provide a semantics for linear logic and are useful in understanding concurrency.
You might have a look at section 1.39 in "Categories, Allegories", by Freyd and Scedrov. They introduce a language of diagrams and show how common definitions can be represented this way. Not a particularly easy read.
I believe for many of the same reasons that Lisp was used with great success in the past. OCaml is descended from the ML family of languages and grounded in solid mathematics, like Haskell. In the hands of the right person it's a formidable tool and arguably provides barriers to entry for competitors.
A topos is essentially a cartesian closed category with a subject classifier. In Set this is the two element set of 1/0 which is a Boolean algebra and thus the internal logic of the category Set is classical.
In general though the subobject classifier is a heyting algebra which expresses the semantics of intuitionistic logic.
There is also a very good, but introductory, book by Goldblatt on Topoi that covers this logical aspect
So in terms of logics the category of Sets is the exception.
By internal logic I mean that for every topos one builds up a theory using it's objects and function between them. An equivalence theorem (see J. Bell) states that a given topos is essentially equal to the category generated by this internal theory.
This program began with Lawvere who noticed that conjunction and implication were really adjoints, the same one as between the product and hom functors in a cartesian closed category.