elixir-maybe VS cardano-ledger-specs

I mean, I could be ignorant about Elixir, but the first thing you do when programming in a language like Kind, Agda, is modeling your problem with types. Everything follows from that. Elixir doesn't even have sum types! It seems like you can't even express very basic concepts like List, Either, Maybe, List, Monad directly. Let alone more sophisticate concepts like subsets, propositional equality, logical negation? I see libs like this which "implement" half-baked, wrong versions of these concepts in contrived ways. Let me know if I'm wrong, but if you can't even translate the first lines of a Kind program in Elixir, I really can't see it as the same thing, at all. Not being elitist! Just saying these are not the same - and that is okay.

Integrates with the ledger, consensus and network components that power the Cardano network. (These are also written in Haskell, and we work closely with these teams.)

I'm not a big Cardano fanboy but this doesn't appear to be the case https://github.com/input-output-hk/cardano-ledger-specs/commits/master

Another thing I should mention is that, if you look at the Cardano smart contract integration formal specification, it actually contemplates the potential co-existence of multiple smart contract scripting languages, of which Plutus V1 is merely the first one.

32 bytes long

https://github.com/input-output-hk/cardano-ledger-specs/blob/master/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/API/Wallet.hs#L70

This is the repository with the ledger specifications: https://github.com/input-output-hk/cardano-ledger-specs