Thread by @VictorTaelin

Since I've been receiving a bunch of DMs asking what HVM, Kindelia and Kind are, and since it is still so early (we don't even have a pitch deck yet!), let me make some tweets to present our work, and a sneak peek on the crazy things we're building. *GIANT TECH THREAD INCOMING*

First, the origins: I'm a huge programming language theory nerd who spent years trying to understand "the true nature of computation". After trying every esoteric language imaginable, hacking λ-terms, and wondering why Haskell is such a slow λ-calculator, I found a curious paper.

It was from 1997, by Yves Lafont, who attempted to answer that very question with a genius take: the fundamental laws of computation are "commutation and annihilation". From that insight, he derived a new model of computation, the Interaction Net. The problem is: it was TOO GOOD.

The Interaction Net is inherently parallel, memory-efficient, high-order, mathematically elegant in a way that nothing else is. It is capable of computing λ-terms exponentially faster than existing λ-calculators(!) and it supersedes Turing Machines and Automata in several senses.

So, what does all this mambo jumbo means? In lawman terms, this suggests that there is a different, unexplored approach to designing computers, processors and programming languages that, in theory, could be much superior to the way we do it today.

Have you noticed how GPUs have 1000's of cores, yet most programmers still write sequential code? Why? Interation Nets could be the key to unleash all the massive parallelism potential that we're missing, and put humanity right back on Moore Law's track.

Since this is such a compelling idea, I've tested it. First, I've developed SIC, a λ-Calculus alternative based on this new model of computation. I then used it as the basis to build HVM, a new general-purpose runtime capable of running programs in a massively parallel fashion.

So, did it work? Yes! Absurdly astonishingly yes! First, I attempted to run functional programs on the HVM. My 1-month silly prototype outperformed GHC, the state-of-art functional compiler used by most Haskell-based companies, in several real-world tasks... by more than 300% (!)

Then, I wrote a dependent type checker on HVM called Kind, and it significantly outperformed every proof assistant in the market (Lean, Coq, Agda, Idris). For these who don't know, this field is trying to "digitalize math" and let computers verify theorems/proofs automatically!

I then tried to apply HVM to the context of blockchains. By swapping the EVM by the HVM, I built Kindelia, an "Ethereum clone" that has 100x to 1000x increased throughput in opcodes like SSTORE. This would be enough to, say, run MMORPGs on layer-1, which is unfeasible today.

Right now, we're looking into compiling Elm to HVM, and run it on the GPU. Imagine writing 3D games and shaders as pure "Pos -> Color" functions, and it just works? That'd be insane, and I have a prototypal CUDA runtime that achieved linear speedup, suggesting that's possible!

Another insane application of the HVM, which this tweet is too short to explain, is its ability to run certain functions exponentially faster than expected. Here, we compute 2^N compositions of boolean NOT in linear time! Could it solve important number theory problems?

Of course, not everything is flowers, and there are some negative results. For example, there are some (avoidable?) cases where the HVM is quadratically slower than GHC. Also, there are some (esoteric!) λ-terms that it can't reduce soundly. It doesn't fully replace GHC (yet?).

Also, and of course, the non-asymptotic speedups come mostly from the fact HVM uses more cores than GHC, so that's obviously NOT a fair comparison! A properly optimized parallel C or Haskell program would outperform the HVM (for now!). But that's not the point!

The point is that HVM programs scale horizontally with *no effort*. Writing correct parallel algorithms is very hard, and that's the main reason humanity under-uses parallelism. On HVM, you write a normal program, you get a massively parallel executable. Nothing else does that!

Also, it is very easy to come up with benchmarks that show what you want to see, but it is hard to even come up with cases where HVM performs poorly. The results are overwhelming and consistent across many areas. Our code is open source and anyone can replicate our results.

So, what's the plan? For now, I've founded a company aiming to develop HVM and explore its potential, build short-term applications (like runtimes, type-checkers, shaders and blockchains), and pave the way for a future where interaction nets run on the hardware.

A friend and I have invested about 100k USD in this company each (for now). I've hired a small team of devs who are, right now, working on building and exploring the applications highlighted above. We also have several other applications in mind, which we intend to explore later.

While I'm a huge tech nerd, I'm not an entrepreneur, and I'm not in touch with the tech startup scene (which is null in Brazil), so I still have a lot to learn to set things up correctly. That said, the current team is insanely good and I'm very excited to see what we'll build!

If you want to be part of this crazy idea (or ask any question), just reach me via DM here. We'll start looking for funding and partnerships soon, so this is the absolute best moment to get involved. And if you just want watch GPUs burn, retweet and spread the word. Do it now!

Have you done it? Thank you! Here are some cool links:

HVM, the parallel runtime
github.com/kindelia/hvm

Kind, the proof assistant
github.com/kindelia/kind

Kindelia, the smart contract platform
github.com/kindelia/kinde…

SIC, the calculus behind HVM:
github.com/victortaelin/s…

A last disclaimer: the published version of HVM only parallelizes very specific programs. The upcoming version (V2) will bring the completed algorithm, which generalizes to almost anything. You can install the branch, or wait a few weeks for its official release.