Can we see proof that Haskell is the correct choice?

There are lots of claims that Cardano is “safer” than other languages and fast. Its the perfect speed and safety language yet the aviation, healthcare, military contractors don’t use it. In fact almost nobody uses it. Ask yourself why.

There are video’s about how mathematically the Haskell language is pure. Unfortunately this leaves a taste of mathematician and not computer scientist in my mouth. You need correct logic but you also need correct implementation. But that is not it. You need to know the hardware your running on keeps your software stable. You need to know the linker produces good executable. You need to know the low level software implements the high level software correctly. Knowing all of this in a paper is an impossibility. Therefore any claim of correctness shows a wild lack of expertise in the field.

As a 30+ year veteran of safety critical software I know that you must test the system functionally and structurally right down to the hardware. The verification if done right should cost more than the implementation because there literally is more work to do.

Anybody trying to convince you that a language is inherently “safer” is blowing smoke up your pants.

Given this position please shut me up with proof you are doing verification from end to end.

If this proof does not exist then give me the names of the board of directors so that I can convince them they are on the wrong track with Haskell. It may be the correct path, but no proof has been offered except that the math works. “The math works” is so not the right answer.

1 Like

Is any other crypto currency’s system proven according to these requirements? Do they do end-to-end verification?

Yes, the code, verifications, where they exist, and the relationship to the mathematical formulation of the protocol could be much better documented.

But if others don’t do a much better job in verifying their systems, it boils down to a matter of taste in the worst case. Actually, a little better, since functional programming languages, while they of course do not guarantee absolutely correct software, do prevent some errors from happening, give a lot of assurances simply through their elaborated type systems etc. pp.

In the end, Cardano is on the one hand (hopefully) already decentralised enough that you won’t find a “board of directors” that can just decide that. And on the other hand, choosing another crypto ecosystem building on a technology more to your liking is probably simpler than convincing a community of ripping everything apart and starting from scratch.

“Nobody uses it.” is quite a misrepresentation, by the way.

1 Like

So the answer is that Cardano is no more secure/safe or verified than any other coin. That gives me loads of confidence.

For all that you know there is a giant hole that a hacker could walk right in and drain all wallets.

Your claim of “actually a little better” is completely false. You don’t know that. That isn’t how security works. Linux guys used to say the same thing…and now we find out a huge hole has existed for a long time. Same crappy attitude and platitudes.

If “nobody uses it” is quite a misrepresentation then you can easily list 150 companies that use it as their primary language to produce a product? Right? < 150 == nothing

I usually don’t smack people down so hard if they actually present a logical argument, but your response was all fanboi.

1 Like

Hello @skeletor53818

The reason Haskell was chosen is because Cardano systems are based on scientific peer reviewed research.

In order to translate all that research into a system protocol you need to use 1:1 mapping with least amount of side effects. Since Haskell is just Lambda Calculus that is expressed as a programing language it is a prefect choice to map focused research and mathematical proofs into a code.

This allows maximum adherence and almost 1:1 mapping with out any artifacts making their way into the proposed research.

As for security, Haskell has static types. It validates code during coding phase so many errors don’t even get to compile or QA phase.

It has immutable data. As you know mutable data and global states are error magnets. Haskell deals with all of that.

Memory safety is also excellent in Haskell (compared to C++). No buffer overflows or memory leaks (unless it’s a hardware issue) like you would get in C++

Plus it’s a lazy language so way easier to maintain over time.

Does any of this means that Haskell is better or worse then any other language? No.

But it makes it a perfect language to build a base layer for research based network that is implementing peer reviewed research into a code.

The fundamental technical base that Cardano is created from and direction is going to is 1:1 mapping of peer reviewed research. So, that is the only consideration that should be relevant in choosing which programing language to use for base layer.

So if you are just comparing languages to each other you may not see the reasoning to why Haskell is chosen.