bitdiddle

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.

There's a new feature, rooms[0], that allows members to replicate with one another and stores nothing.

[0] https://github.com/ssb-ngi-pointer/rooms2

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.

Dan Weinreb had a different take on the symbolics era and the MIT lab.

[1] https://danluu.com/symbolics-lisp-machines/

https://scuttlebuttbrewing.com/

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.

yes, revocable and irrevocable trusts, combined with solid powers of attorney, living wills, etc..

Trusts essentially keep estates out of probate. Since it's the money these criminals are after they work well towards that goal.

estate planning

It's all down hill from here. Pretty soon there will be a 2K word minimum and we'll all be making up stuff, like those fifth grade book reports.

gotta love this line:

"We aim to be a drop-in replacement with bug-for-bug compatibility."

"30. In programming, everything we do is a special case of something more general -- and often we know it too quickly."

my thought exactly, memo to marketing :)

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.

[1] http://boole.stanford.edu/pub/ratmech.pdf

Nice to see how efficient this non-profit is (8% overhead).

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.

Symbolics workstation

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.

Buy some of the stock, you'll feel better :)

Agreed, this is much like the situation in the 80s, and generally a good thing.

The only question I would have is what happened to export controls of capital? Is all this money legit? Cash is king I guess.

I would include Guile in this list of lisps :)

+1

I couldn't agree more. My first boss gave me the HP-12C as a year end gift back in 1985. I still use it once a week or so or anytime I need to do a bond calculation.

I'm still on the original battery, kid you not! I love the feel of the keys.

Noah Warren - http://www.poetryfoundation.org/poetrymagazine/poem/248624

hmm, it seems to me that the author confuses NP-hard and NP-complete in a couple of places. Typos perhaps, or just poorly written.

Brian Eno makes a good argument[1] that it's already here.

[1] http://edge.org/responses/q2015

+1

There's some interesting theoretical work that was done by Srinivas in the 90s[1], that takes a geometric view of pattern matching, based on sheaves, and uses it to derive a generalized version of KMP that can be applied in other domains. I'm not sure what happened to this research program, and forget most of the details, but I heard a talk by Srinivas and recall thinking it was a very practical and real application of category theory.

[1] http://www.sciencedirect.com/science/article/pii/03043975939...

+1

Your comments in this thread have really piqued my interest enough to read some of this HoTT. I'd heard of this a couple of years back and didn't have the energy for it at the time.

Some years ago I spent a serious amount of time reading topos theory, particularly local set theory, as given by the Mitchell-Benabou internal language of any topos, looking for a better approach to description logics.

I do believe topos theory provides a better foundations than set theory because the logic is inherently intuitionistic. I found it also provided a simpler explanation of independence results. However one of the things I believe is true of the proof theory is that there is no cut-elimination theorem, which is important to establish a sub-formula property.

Sorry to ramble here, let me ask specifically, are there connections between HoTT and topos theory? Or geometric logic? Your earlier comment on the synthetic nature made me think there might be.

Thank you

Edit: I more or less answered my own question by reading the introduction, the section on open problems, the possible connections are between HoTT and the higher toposes. Judging from the intro, this seems very readable.