Cardano updates and understanding: Why Haskell?
Thank you @Gandalf for this video!
All hail Letās Talk Cardano!! Heās back!
The clips in this video are well placed, I like the editing style, good job on #7.
Thanks
I subscribe to your podcast on iTunes, but I havenāt seen this one uploaded. Do you plan to upload it at some point?
Plutus compiles to Plutus Core, and Solidity will compile to IELE.
It is clear that Solidity will be supported for combatibility reasons. But they do not like Solidity so much. They will not recommend it anyway. So why support interoperability to something that is in their eyes so much inferior? It might spoil the whole platform ā¦
Yes. I plan to put it on the audio podcast. Just need to convert the file. Expect it in the next 24 hrs
I think the reason is the momentum behind Solidity. When you weigh it all up itās not a bad idea to support multiple languages IMO. I suspect more devs will be able to contribute with more available languages. There is probably solidity code that has been battle tested rather than being formally verified.
IMO new highly secure contracts will one day be formally verified (built in plutus first) before being let out into the wild.
Haskell is a really good FP language, unfortunately we need more (good) devs on this field, the mainstream adoption is still lacking. I wonder if thereās a plan to work with institution to promote the language more as well as start creating libraries. One of the reason R language is so popular is the wide support from the institution as well as a large number of libraries.
IOHK advertised a position a while back to work on Haskell libraries within the Blockchain Laboratory of the University of Edinburgh.
I see two possibilities:
- Haskell is just ātoo good to be trueā. Mass adoption impossible, because the average programmer cannot handle it => a huge impediment for the cardano project
- Haskell is gradually gaining traction. Young programmers will replace the older ones as time goes by, and the youngsters will pick up quicker this complex stuff. Also, languages like Haskell (functional) are much better suited to deal with complex problems as we find it in the blockchain area. So Haskell will just succeed because it enables things that would just remain unreachable without it.
Choose option 1 or 2 as you please! I just have no clue myself.
Yes of course, it is a ābackward compatibility thingā, but of course cardano does weaken own principles by allowing a technology that they consider inferior to their own.
However, as KEVM is defined by the K-Framework, shouldnāt it be possible to formally verify a smart contract written in Solidity, once it has been compiled to KEVM?
I would think both scenario are possible:
-
average programmers are not used to handle the āweirdā syntax of Haskell, but this wouldnāt stop the adoption of Cardano itself, as you mentioned, thereās always the K framework that would eventually allow the more āmainstreamā developers to be able to create applications on top of the framework.
-
on the other hand, we would still need to preach Haskell more in universities all over the world, and Iām sure that IOHK is working heavily with institutions such as University of Edinburgh, as well as universities in Africa, hopefully IOHK would extend that to USA, China and India as well, the sites of largest concentration of developers in the world with great Computer Science programs at the respective countries, such as MIT, Stanford, Indian Institute of Technology, TsingHua U.
-
additionally, we can also have the instructors teaches Haskell via media like Coursera, DataCamp, etc. Iāve heard that the team went to Africa and educate the people there, but online teaching would probably be useful as well
The cardano settlement layer (CSL) is meant to be written in Haskell, is it? So, for any other layers it would be about interoperability and interfaces to many more programming languages, correct?
If there is a shortage of Haskell developerās in Cardano at the moment: These people are needed just for the CSL. Everything else would come later and would open up to the majority of āordinaryā developers (like me)
The CSL is somehow out of my scope. I would be way more interested in real world use cases that can be implemented on top of the cardano platform => Too early! Wait until the Haskell guys have finished ā¦
I believe it is possible, but wayyyy harder. My understanding that formal verification is no walk in the park, even using haskell.
OK, it is getting clearer: Formal verification will remain difficult, even for smart contracts written in Plutus I guess. Also it is optional. That is why the situation here is different to type checking in a fully typed programming language, where types are ALWAYS verified by the compiler. Formal verifcation seems to be an additional step, and again, one might be trapped in complexity, as with Haskell.
Maybe yet another layer would be needed, on top of the smart contracts, to make formally verified smart contracts really accessible ā¦
[quote=ālyrx1, post:17, topic:12265ā]
to make formally verified smart contracts really accessible ā¦
[/
Indeed, that would be great