3 ms·

Here is a project that uses F* (another language with dependent types) for proving cryptographic algorithms. https://project-everest.github.io/ https://project-

Here 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 ago
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 :)