Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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

1: https://www.idris-lang.org/



Here is a project that uses F* (another language with dependent types) for proving cryptographic algorithms. 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.


F* 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 :)




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: