What are real world examples of dependent types signficant improving security or productivity?

This page summarizes the projects mentioned and recommended in the original post on reddit.com/r/agda

Our great sponsors
  • Scout APM - Less time debugging, more time building
  • SonarLint - Clean code begins in your IDE with SonarLint
  • SaaSHub - Software Alternatives and Reviews
  • CompCert

    The CompCert formally-verified C compiler

    Check out CompCert C compiler. It's your usual C compiler but with all optimizations verified to be correct (i. e. not changing program semantics). This means that as long as you agree with definition of program semantics given in the compiler (it's reasonable) and believe that Coq - the dependently typed language behind CompCert - is correct, you can be sure that no optimization breaks your code and that's a big deal since program optimization algorithms are very prone to bugs in usual compilers.

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts