Why did IOG choose Haskell to build Cardano?

English Education
1

The IOG team carefully decided which programming language and tools to use for Cardano development. In the end, they chose Haskell. The team must be able to formally verify that everything written in the white papers will correspond correctly with the source code. Come read about how the team transforms the mathematical proofs from the white papers into Haskell source code.

TLDR

  • Before Cardano, no project from the top 10 used formal methods.
  • The white paper is the basis for the formal specification. It is the basis for the source code written in Haskell.
  • The formal specification and Haskell source code have very similar notations.

This article was prepared by Cardanians with support from Cexplorer.

Read the article: https://cexplorer.io/article/why-did-iog-choose-haskell-to-build-cardano

1 Like
2

As already with the last article

I would not use this point in marketing too prominently, if it has not been done.

There are no formal verifications of the source code to be found.

It is not documented how the peer-reviewed papers are implemented in detail by the real-world Cardano system. (In addition to the fact that academic peer review is also not as high a standard as many non-academic proponents of Cardano seem to believe.)

More humbleness would be great.

3

Happy cake day @Jaromir

2 Likes
4

Thank you!

5

As far as I know, one of the key developers (the wizard) talked about critical parts being created through formal methods. Of course, this doesn’t apply to all parts of the project, as it would take too long to finish the development. On GitHub, you can find formal specifications for at least some parts of the project. I did not check all repositories.

2 Likes