wisnesky

8 ms·

31.
by wisnesky 6y ago
You are right that computer generated proofs are often tough to understand, and that understanding is often the intended goal of writing a proof. But proofs can be useful for reasons besides human understanding, especially so in engineerin
32.
by wisnesky 6y ago
Many such lists exist. For example: https://en.wikipedia.org/wiki/List_of_statements_independent...
33.
by wisnesky 6y ago
It is true that Godel's incompleteness theorem states that there is no complete axiomatization of arithmetic; no first order axioms can characterize the natural numbers up to isomorphism. But Godel's completeness theorem ( https
34.
by wisnesky 6y ago
Honestly; I'm not sure; I'm a working computer scientist, not a working mathematician, and I use a proof assistant (Coq) all the time to have confidence that the proofs I write are correct (and more and more this is a requirement
35.
by wisnesky 6y ago
Much of theoretical computer science uses categorical methods, for example, as semantics for type theory. In that field, such techniques are often more natural than set-theoretic ones due to issues of computability, decidability, etc. So
36.
by wisnesky 6y ago
We're using applied category theory quite heavily in the design and implementation of the categorical query language CQL: https://www.categoricaldata.net . There category theory gave us algorithms that are missing from SQL
37.
by wisnesky 6y ago
You must be referring to the "love-hate" relationship between Amazon and open source software as described eg here? https://www.zdnet.com/article/amazon-and-commercial-open-sou... "Vendors developing tho
38.
by wisnesky 7y ago
In 2020, software is reliable?
39.
by wisnesky 7y ago
Your point is well-taken, and being overlooked, so here it is explicitly: to implement "wet. messy business logic" is, by definition, to implement "a complex algorithm".
40.
A new, non-Apache open-source revenue model(slideshare.net)
8 points by wisnesky 7y ago|1 comments
41.
A Multi-Model Abstract Data Type and Economic Engine [pdf](rredux.com)
18 points by wisnesky 7y ago|0 comments
42.
by wisnesky 7y ago
Yes, Coq is pronounced like "cock" in English. C'est la vie
43.
by wisnesky 7y ago
Many people on this thread have asked if there is a rigorous way to migrate data between relational schemas that contain non-trivial foreign keys, and the answer is yes: In the open-source categorical query language CQL, data migrations nec
44.
by wisnesky 7y ago
I agree, whether or not a given data model has foreign keys is a math question with a correct answer (up to isomorphism of the data model); if it does, where in a system they should or should not be enforced is an entirely separate, impleme
45.
Mm-ADT VM integrates query languages, processors, and storage systems(mm-adt.org)
1 points by wisnesky 7y ago|0 comments
46.
Reddit AMA: Brendan Fong and David Spivak about Applied Category Theory(reddit.com)
3 points by wisnesky 7y ago|0 comments
47.
Is the Equal Sign Overrated? Mathematicians Hash It Out(wired.com)
2 points by wisnesky 7y ago|0 comments
48.
by wisnesky 7y ago
Kevin Redwine: Inference Rules Plus Proof-Search Strategies Equals Programs (2009). http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.152.... In the programming-language community many authors communicate algori
49.
by wisnesky 7y ago
No, those result numbers do not include quotation marks. With the quotes I show the same results as you.
50.
by wisnesky 7y ago
I'm showing 1M and 200K Google results for those phrases, respectively.
51.
by wisnesky 7y ago
I'd be happy to showcase our recent progress. But let's connect offline, so as not to hijack the conversation. Feel free to drop me a line at ryan@conexus.ai.
52.
by wisnesky 7y ago
Absolutely, and I would encourage you to contact us offline first to discuss related work in this space - there is indeed a lot, because the category of CQL schemas forms a BCCC and for each schema S, the category of S-databases forms a top
53.
by wisnesky 7y ago
There is up to $1.5M USD available for start-ups who want to solve business problems with category theory: https://conexus.ai/ventures and there is an open-source implementation of the data migration sketch from that book h
54.
by wisnesky 7y ago
Here is a short course on applied category theory: https://ocw.mit.edu/courses/mathematics/18-s097-applied-cate...
55.
Categorical Query Language(categoricaldata.net)
11 points by wisnesky 7y ago|0 comments
56.
Applied Category Theory Meeting at UCR(golem.ph.utexas.edu)
4 points by wisnesky 7y ago|0 comments
57.
by wisnesky 7y ago
Indeed, we (David Spivak et al) are (among other things) trying to apply those seven sketches in applied category theory to business problems and are soliciting proposals for up to $1.5M in venture funding from interested start-ups to do so
58.
MIT spinout offering $1.5M to ventures in Applied Category Theory(reddit.com)
8 points by wisnesky 7y ago|0 comments
59.
MIT spinout offering up to $1M to ventures in Applied Category Theory(conexus.ai)
1 points by wisnesky 7y ago|1 comments
60.
by wisnesky 7y ago
Check out http://categoricaldata.net for a categorical approach to database theory that uses a labeled null semantics from type theory.

More ›