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 /r/agda

Our great sponsors
  • WorkOS - The modern identity platform for B2B SaaS
  • InfluxDB - Power Real-Time Data Analytics at Scale
  • 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.

  • WorkOS

    The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

    WorkOS logo
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