A startup in a programming language derived from homotopy type theory raises $10M by 2030
Standard
16
Ṁ4772030
26%
chance
1D
1W
1M
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
Get
1,000
and1.00
Sort by:
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
10B valuation for company founded by a 2023 Thiel Fellow by 2030
33% chance
1B valuation for company founded by a 2023 Thiel Fellow by 2030
55% chance
Will Ada Nguyen raise at least $100k for a startup by 2024
41% chance
A least twenty Thiel fellow founded companies are estimated to be worth >1B USD before 2034
67% chance
Will more than 15 percent of the thiel fellowship 2025 be hardware startups
47% chance
Will OpenAI have >$10 billion in revenue by 2030?
86% chance
Will an Atlas Fellow launch an AGI startup worth >$1 million by 2030?
92% chance