My unedited, uncensored thoughts about Ethereum, Cardano, Tezos, formal proofs and functional programming being a gimmick

*Warning: this post is a huge wall of unedited thoughts. *

When browsing another thread on this subreddit, I've noticed a comment about Cardano from /u/Theory-Early, who wrote:

I dont think it sounds promising at all. 99.99% of all programmers do not give a single fuck about functional programming or formal verification. it's literally a gimmick to scam non-programmers with an ICO.

programmers aren't attracted to cardano, only fucking retarded investors who think functional programming and formal verification is some magic bullet.

First of all, Cardano is a mess that does not represent how a functional blockchain should be made. But I'll talk about this subject later. For now, I'd like to talk about the "FP is a gimmick" part. Rather than getting offended and discard /u/Theory-Early as someone who just "doesn't get it" (like most FP elitists would probably do), this inspires me to really understand where this perception comes from, evaluate its merits and wonder what could be done to change it. This isn't just an isolated case. When I was developing Formality, I've felt that impression coming from many of you, and I know many of you feel that way. Rightfully so, ok? It is my job to understand this feeling, its roots, and figure out how to change it.

It is true that functional programming and formal verification has certain fame of being over-hyped tools that, in the end, provide little to no practical benefit. At the same time, those who do get it ultimately fall in love and almost universally come to the conclusion that it is objectively, profoundly superior to the alternatives. Isn't that weird? Why there is such a huge disconnect between people who "get it" think it is the best thing ever, and everyone else, who just watches from the outside and judges it as a useless gimmick?

I think both sides have a fair judgement. The thing is, when you, in a personal level, learn about FP, you instantly realize how good it is. It is obvious for you, because all the tools it directly provides you objectively make you a better programmer, today. You get access to abstractions like functors, monads, folds, composition, a next-gen type-system. Learning to use these things properly makes you so much better that you wonder how you could ever lived so long without those things. And then you start preaching about how amazing FP is. And write about burritos. And ultimately proceed to build nothing of real value.

Ah, that happens sooo often. But why? If FP is so objectively better, where are all the cool things built with it? I have a simple answer to that paradox, but it might make some people really upset with me: Haskell isn't a practical language. And that's all.

See, there are some practical FP languages like Scala and Clojure, but these are practical exactly because of all the non-FP concepts mixed in. They are hybrid, multi-paradigm languages. So that doesn't count as a solid argument in favor of FP. When it comes to fully embracing FP, there is only one mature language in the market: Haskell. And that language isn't practical. Simple as that. I hope that doesn't make /r/haskell upset with me, but, as much as I love it, it isn't.

1. Haskell has possibly the worst package manager in the world. It is not just bad, it is terrible. As in, "can't install more than 3 libs without breaking the world" terrible. It is so bad the community had to create a second package manager that maintains a curated list of packages that work in conjunction. Which kinda works, but 1. requires a ton of work, 2. doesn't scale and 3. still breaks if you need to install anything outside of that curated list.

2. Its error messages are sometimes great, sometimes completely cryptic. Problem is: it takes just one cryptic messages to waste hours of your time. Even worse, in the end, often it isn't even your fault. Which takes us to...

3. A messy soup of package extensions that is required to make up for the lack of dependent types. Sooner or later, something you need to do will not work just because Haskell can't understand it. And then you'll need to add extensions like RankNTypes, GADTs, FlexibleInstances, ScopedTypeVariables, and eventually you're coding in a frankenstein dialect with error messages that not even the author understands.

4. Too many obscure, academic words that exist for historical reasons (or no good reason). This only further isolates the community in a bubble. If a word requires explaining, it isn't a good word. A programmer shouldn't learn a whole new vocabulary to just get started. Things like: why isn't Functor called Mappeable?

5. The idiomatic syntax isn't very practical. For example, a fold is beautiful when the body is short, but when it is large, it requires you to indent your code in bizarre ways. See this comment for an example. The acclaimed point-free style often leads to unreadable one-liners that do 1000 things. The equational notation for function declaration becomes redundant once you have many arguments, and it doesn't scale vertically. Monads are a genius, profound way to handle effects... once you spend a semester learning about them and getting overwhelmed by the awful or plain wrong tutorials. Pattern-matching records with many fields requires you to rename all fields, every single time. Extracting big or deep fields is extremely verbose, almost forcing you to deal with lenses. Which then require another semester of courses, 10's of cryptic symbols, and once you do it, have fun with your 10x performance penalty. And then you miss the times when you could just write foo.bar.x.y += 3.

6. Finally, and perhaps mostly, its failure to compete on the front-end, user-facing space. There is still no viable JS compiler, no satisfactory way to make iOS/Android apps, or Windows/OSX/Linux releases.

In short, what I'm saying is that Haskell is a very unpractical language out of the box, and that it is a major contributor to this perception that FP is a gimmick. And don't get me wrong, I'm not hating on Haskell, it is still one of my favorite languages, and it can be extremely powerful for an individual or isolate team with enough time. But I truly don't think it is going to, say, replace TypeScript anytime soon. It just doesn't scale, community-wise. And what is the point of being a god-like programmer, in a language that few use? Only to get beat by a CS freshman who just installed a npm package that does what he wanted?

But FP, as a concept... that's a different matter. It has a lot of potential, and I don't think anybody will be able to judge it until they truly get it. So, this sparks the question: what would happen if we had an catual hardcore functional language, with all the power of Haskell, but none of its practical problems? I.e., one that would be as easy to learn as TypeScript? One that would strip away all the academic jargon, one with amazing error messages, one with an easy, obvious ways to anything you do in conventional languages (effects, field updates, loops)? One that, like TypeScript, was ready to scale into a massive ecosystem of real-world applications? Yet, one that, under the hoods, was grounded on the solid foundations of type theory, with dependent types, formal proofs and all that powerful stuff waiting for you, when - and if - you're ready for it? If we had such a language, what would happen? Would the common developer still dismiss FP as a weird thing of weird people, or would they suddenly realize the immense power that FP has, and fall in love? I honestly, deeply, strongly, think the later would happen.

Am I right? Am I wrong? Well, for one, we could almost see that happening a few years ago, powered by another language: Elm. It did just some of the things I sad, and the result was clear, as it quickly grew to be one of the most used functional languages. But it had a big issue: it simplified things so much, it ended up shallow. Once you learned enough and started needing the additional power, it wasn't there. The language was too limited to do certain things. So the hype eventually died off. But do you really need to overly simplify the core language in order to make it simple? No! I don't think so. You can just be careful to get these things out of the way of the common developer, and that can be accomplished by serving the common developer a familiar syntax that is just enough for him to thrive. The advanced stuff can still be accessible for those who want it.

This line of thought is what ultimately lead me to build Formality, now named Kind. Kind is the language being developed with the main purpose of becoming the ultimate functional language that can scale to the wide market, maintaining all the power of Haskell, fixing its mistakes, bringing powerful concepts from proof languages and keeping itself approachable, efficient. Are we there yet? Honestly, I think we are. At least, very close. A solid foundation? Check. Performance? Check. Can it be used by normal developers to build real stuff? Well, in the last few months, I've made an experiment. I've hired about 5 individuals with little or no programming experience, taught them Kind, and asked them to build a game and left. 3 months after, they're almost done building an engine with rollback netcode, a graphics framework, a reactive user interface, state computations based on stream of events. They're dealing with monads, folds, dependent types. And they just keep building and giving, not ever getting stuck or feeling hopeless. I truly think no other proof language has accomplished anything like that.

So, why this big wall of text, here on /r/ethereum? I actually don't know. I guess I had too much to say, and I wanted to vent. I do feel a little anxious when I see idiots getting so much voice and attention, but nothing gets me more than projects that have no substance or fundamentals getting treated as if they were somehow profound. Doge deserves its spot, it has a foundation, for being a meme, for being cute, for challenging the seriousness of money. But Cardano? What is its foundation? It sells itself as a more functional, research-based alternative to Ethereum. So, please, can anyone tell me one thing Cardano does, that Kind+Ethereum doesn't do much better? It makes me upset to see people dismissing FP as a whole, because of a project with no real substance, that promises to change the world, yet can't deliver smart-contracts after half a decade of existence. I think Cardano is a big disservice for the FP community.

When it comes to formally verified smart-contracts, Kind+Ethereum is all we ever need. And, no, I'm not saying formal proofs are a silver bullet for security, but I do think it will massively improve the issue, and I promise eventually you'll get it. But how? For some time, I thought it'd be a matter of compiling Kind to the EVM. That would allow you to write normal Kind programs and run them inside Ethereum. I don't think that is a great idea anymore. The gas overhead of compiling lambdas, as little as we make them, is still superior to 0. In a network where every opcode costs a fortune, people would just write in a cheaper, less safe language. And, in reality, smart-contracts are often simple and don't require all the features you have in Kind.

So, for now, the plan is to just create a SmartContract DSL on Kind, with a reasonable syntax sugar, that will allow people to write Ethereum smart-contracts embedded on it. They'll then be able to easily deploy, monitor and prove things about these contracts. Simple, easy and effective. Sure, this is something that can be done on Agda, Idris, Coq too. And perhaps that is why I've avoided this solution for a while. But, honestly? That is the way to go. And these are not practical languages either, I don't think they'll ever have massive ecosystems, so doing it in Kind will enable formally verified smart-contracts for the masses, which is something new. Now, please, tell me: once Kind is popular, has a great ecosystem, and people can easily write, deploy and verify Ethereum smart-contracts on it... then what is even the point of Cardano anymore? In what technical sense it even needs to exist? It doesn't scale better than Ethereum, the built-in forking stuff is an actual gimmick, and it isn't safer or more functional in any way. So I honestly can't find a reason. If anyone has a great answer to that question, let me know, because I've been waiting for years and there is none.

To be clear, I don't want to sound like a hater. I'm not lying when I say I love when I'm proven wrong, because I can cut losses and stop wasting my time in a wrong idea (just be Kind, please). But for now, I can't look at Cardano and not think: what is the point? Or, rather: why people are so hyped about something that is, in my head, objectively inferior to what I'm building? Am I that out of touch? I'm just trying to understand. What Cardano does? The best arguments I've found so far are that:

1. "Haskell is safer than Solidity." Fair. But Kind is much safer than Haskell. By a large margin. Is there anyone who disagrees with that? So, are you telling me that Cardano built an entire network, with the whole premise of being "a safer, more functional" alternative to Ethereum, only to be obsolete as soon as an actual proof language adds support to Ethereum smart-contracts? Or are they betting that a proof language like Kind will never be popular enough to be viable? Or that people will never realize Haskell doesn't even have formal proofs?

2. "Our virtual-machine language is easier to reason about." Fair. But a DSL in Kind, that compiles to the EVM, can also be made very easy to reason about. There is no need to create a whole network around that. Now, to be clear, I still think compiling Kind to its own INet-based "functional virtual machine" is a fucking amazing idea. That would justify building its own, separate blockchain, because the cost model is so beautifully great. But that's a lot of work, and NOT what Cardano is proposing.

To be fair, I could be really misunderstanding something, since Cardano smart-contracts aren't even written in Haskell, and it is still not clear to me what is the actual language used for it. Is it Plutus? Is it Marlowe? What is the execution environment that every full node runs? Is it a stack-machine? Are there lambdas? What are the opcodes? Where is the cost table? Is there even one? How much a beta-reduction costs? How do they measure that? Perhaps I'm too dumb to get it, but, I mean, if I can't get it, how do they expect everyone will? It has been years and I still don't get Cardano. And I swear I'm not lazy, I've tried. For a comparison, it took me a 5 minutes to open Ethereum's yellow paper and immediately get its point.

Anyway, these are my un-edited thoughts about all these things, for whoever this may interest. About Kind, soon we'll be back with a bunch of cool things to show. I just hope people give us some space to show these things! If Cardano deserves a $54b network, we deserve some attention. It is so sad to see crap getting so much attention, while people building real stuff gets ignored. But, fair enough, the market decides what it wants. For now, we'll keep building.

See you, eventually.