A startup in a programming language derived from homotopy type theory raises $10M by 2030

Standard

Ṁ477

2030

26%

chance

ALL

Resolves to `yes` if by Jan 1st 2030: 1. A startup is building a product in programming language X ("PLX") 2. PLX _cites_ a paper or book associated with the HoTT movement in its whitepaper or otherwise in its documentation. 2.1. Designers or contributors of/to PLX verbally/twitterly claiming that they're influenced by ideas in HoTT doesn't count. The influence must be substantial and clear enough that citations are happening. 3. That startup raises at least $10M in funding

#️ Technology

#Startups

#Programming

Get

1,000

and

1.00

3 Comments

Sort by:

HoTT is very cool and all, but it is not something that will make you money.

I wonder what this would look like, or how you know if you have seen it? I have heard of HoTT before a few years ago and had the ideas explained to me, but my understanding is between nothing and superficial. I would have thought Coq or Agda would be ok 'programming languages' for this but maybe that is not what you meant.

@Undox I think if some coq project that utilized the coq-hott library or some agda project that utilizes the cubical-agda extension had relevance to prod, it would be valid! But the only coq code I've heard about in industry has used the separation logic facilities, which is quite basic from a pure type theory perspective (I did use the coinductive free monad library `ITree` at an industry gig, but that's not really related to HoTT). I've heard one rumor of agda in industry, and the context was "it was a mistake and a waste of time to try solving our problem in agda". But to answer the question "how do you know if you have seen it", see the resolution criteria: docs or whitepaper must cite a paper associated with HoTT ("associated with HoTT" is up to my discretion; I don't consider everything in the dependent type theory space to be "associated with HoTT")

Related questions

Related questions