What is the need of formally verified compilers? Where are they used? Do verified compiler support all features that unverified compiler do?

This page summarizes the projects mentioned and recommended in the original post on /r/compsci
compcert coq C Compiler

InfluxDB
Our great sponsors
  • InfluxDB - Power Real-Time Data Analytics at Scale
  • WorkOS - The modern identity platform for B2B SaaS
  • SaaSHub - Software Alternatives and Reviews
Our great sponsors

  • CompCert

    The CompCert formally-verified C compiler

    Languages are often not verified in full, because doing so might be a tremendous task, and you often don't need to verify a whole language. Often just a subset of the features will allow you to do what you need to. One example of a partially verified C language: https://compcert.org/.

  • InfluxDB

    Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

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