You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
dan pittman (May 05 2023 at 01:16):(Please feel free to move this, I’m not entirely sure where the best place to put it is)
Hey all, who here is not in academia, and what do you do?! I have worked in the formal methods space in the past, though, for the last 18 months or so have been doing something else entirely (happy to say more if anyone is interested). I’m curious what companies are out there in the FM space and what they’re up to.
Ryan Wisnesky (May 05 2023 at 03:48):there's us at Conexus AI, we formalize databases and similar things using category theory and use formal methods from term rewriting, functional programming, etc, to implement ETL/data integration in provably correct and optimal ways
Steve Huntsman (May 05 2023 at 12:28):dan pittman said:
(Please feel free to move this, I’m not entirely sure where the best place to put it is)
Hey all, who here is not in academia, and what do you do?! I have worked in the formal methods space in the past, though, for the last 18 months or so have been doing something else entirely (happy to say more if anyone is interested). I’m curious what companies are out there in the FM space and what they’re up to.
Tough to beat Galois and/or SRI in industrial research on FM, though of course some of the largest information tech and aero/defense shops also do top-notch FM work.
My shop does some FM work (but I haven't done any here). DM me if interested.
Re: category theory, if I demonstrate a winning value proposition for large cardinals or Langlands or conformal field theory--or category theory--for something that my shop wants me to work on, then that's that. I have accrued a fairly large bag of hammers over the years and despite being an absolute (and relative) dilettante at CT I have been able to fruitfully use it in a few ways, not always indirectly.
dan pittman (May 05 2023 at 15:50):Ryan Wisnesky said:
there's us at Conexus AI, we formalize databases and similar things using category theory and use formal methods from term rewriting, functional programming, etc, to implement ETL/data integration in provably correct and optimal ways
Very cool, this is exactly the type of thing I was looking for. I'm wondering who is trying to productize ideas from formal methods and whether or not they're having any luck.
Steve Huntsman said:
Tough to beat Galois and/or SRI in industrial research on FM, though of course some of the largest information tech and aero/defense shops also do top-notch FM work.
My shop does some FM work (but I haven't done any here). DM me if interested.
Re: category theory, if I demonstrate a winning value proposition for large cardinals or Langlands or conformal field theory--or category theory--for something that my shop wants me to work on, then that's that. I have accrued a fairly large bag of hammers over the years and despite being an absolute (and relative) dilettante at CT I have been able to fruitfully use it in a few ways, not always indirectly.
I am in Portland, and know Galois well! I Interviewed for a job there ~5 years ago, but ended up staying where I was at at the time (auxon.io (where I was last involved in the FM space)). As I think about returning because I miss the intellectual itch it scratches, I find myself interested in not just the theory, but the exposition it takes to turn the theory into a product.
Fabrizio Genovese (May 05 2023 at 19:48): Fabrizio Genovese (May 05 2023 at 19:50):That's what me, @Philipp Zahn, @Jules Hedges, and @Daniele Palombi do. Zero investors, started literally as 'some guys bored with academia', we have a very small amount of grant money coming in, and we are totally revenue positive thanks to good old paying customers.
Fabrizio Genovese (May 05 2023 at 19:51):So if you want an example of a business model that is 'entirely relying on category theory to function' and 'entirely relying on paying customer money to survive', then we check these boxes.
Fabrizio Genovese (May 05 2023 at 19:52):(and yes, I am incredibly proud of this! You can actually sell category theory to people!)
Jules Hedges (May 09 2023 at 16:39):Fabrizio Genovese said:
So if you want an example of a business model that is 'entirely relying on category theory to function' and 'entirely relying on paying customer money to survive', then we check these boxes.
The "entirely" is a slight exaggeration, the majority of the work is not doing category theory... at least not in any sense that most people here would recognise it. The majority of the tech is explicitly category-theoretic, although there's also a few bits where it needs to just go by any means necessary
Fabrizio Genovese (May 09 2023 at 18:22):Well, the tech stack is built on categorical research, implemented in Haskell, which is built on categorical research, and in any talk we give we mention at least en passant the categorical foundation of everything we do (esp wrt to using compositionality in prod)...
Fabrizio Genovese (May 09 2023 at 18:23):Then if you mean it as "we don't say to people 'look, your problem is a morphism bla in the category of bla'" then you are obviously correct, but I don't think anyone would expect that to work
dan pittman (May 09 2023 at 20:16):Fabrizio Genovese said:
Then if you mean it as "we don't say to people 'look, your problem is a morphism bla in the category of bla'" then you are obviously correct, but I don't think anyone would expect that to work
Haha, no, what I meant is exactly what you've said above:
Fabrizio Genovese (May 09 2023 at 20:18):dan pittman said:
Fabrizio Genovese said:
Then if you mean it as "we don't say to people 'look, your problem is a morphism bla in the category of bla'" then you are obviously correct, but I don't think anyone would expect that to work
Haha, no, what I meant is exactly what you've said above:
- Have an idea with formal underpinnings.
- Turn it into a product of some kind so you can keep doing cool and weird computer science / math things amidst the druthers of late stage capitalism.
Then yes, I stand by what I said!
Simonas Tutlys (Jul 19 2023 at 11:37):If industry includes practical open source repositories i wrote a very basic framework where ai models (or anything else optimizable) are morphisms and you can optimize various diagrams.problem is,me being neurodiverse and having issues,i burnt out/blocked myself out from using it but it's my first repo having some cloning activity.it's akin to the modeling work with algebraicjulia but much more simple and in python.julia sounds like heaven to learn but like i said,burnt out.