3 ms·
Stronger assertions can be given by static types. For more expressive assertions, dependent types[0] as seen in Idris[1] are very powerful. When it comes speci
by Legogris 7y ago
Stronger assertions can be given by static types. For more expressive assertions, dependent types[0] as seen in Idris[1] are very powerful.
When it comes specifically to cryptography, I think formal verification should be added for increased confidence.
(I'm not saying "don't bother writing tests if you're using a strongly typed language" - these things can and should be be complementary)
0: https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type
1: https://www.idris-lang.org/ https://www.idris-lang.org/
- AnaniasAnanas 7y agoHere is a project that uses F* (another language with dependent types) for proving cryptographic algorithms. https://project-everest.github.io/ https://project-everest.github.io/ As cool as Idris is, in my experience it has been quite buggy. I would suggest Agda or Coq instead which are more mature.
- Legogris 7y agoF* is rad! Idris indeed still has some way to go to be production ready but I like to give it relevant attention when I can. It's like a reimagined Haskell :)