ISO C became unusable for operating systems development

This page summarizes the projects mentioned and recommended in the original post on news.ycombinator.com

Our great sponsors
  • SonarLint - Deliver Cleaner and Safer Code - Right in Your IDE of Choice!
  • Scout APM - Less time debugging, more time building
  • SaaSHub - Software Alternatives and Reviews
  • dafny

    Dafny is a verification-aware programming language

    You're right that you can't define a safe subset of C without making it practical. MISRA C defines a C subset intended to help avoid C's footguns, but it still isn't actually a safe language. There are alternative approaches though:

    1. Compile a safe language to C (whether a new language or an existing one)

    2. Formal analysis of C, or of some practical subset of C, to prove the absence of undefined behaviour

    Work has been done on both approaches.

    ZZ compiles to C. [0] Dafny can compile to C++, but it seems that's not its primary target. [1][2]

    There are several projects on formal analysis of C. [3][4][5][6]

    [0] https://github.com/zetzit/zz

    [1] https://github.com/dafny-lang/dafny

    [2] https://dafny-lang.github.io/dafny/

    [3] https://frama-c.com/

    [4] https://www.microsoft.com/en-us/research/project/vcc-a-verif...

    [5] https://www.eschertech.com/products/ecv.php

    [6] https://trust-in-soft.com/

  • usbarmory

    USB armory - open source flash-drive-sized computer

  • SonarLint

    Deliver Cleaner and Safer Code - Right in Your IDE of Choice!. SonarLint is a free and open source IDE extension that identifies and catches bugs and vulnerabilities as you code, directly in the IDE. Install from your favorite IDE marketplace today.

  • unsafe-code-guidelines

    Home for the Unsafe Code Guidelines working group.

  • linux

    Linux kernel source tree (by ClangBuiltLinux)

    Linux builds on clang after a decade of dedicated effort to make it happen, and that is with clang overall being comparatively similar to gcc (e.g clang implements many gcc extensions): https://github.com/ClangBuiltLinux/linux/wiki/Project-histor...

  • tamago

    TamaGo - bare metal Go for ARM SoCs

    > just proves your lack of knowledge

    Tone is not needed.

    For TamaGo, it seems to allow developers run their application, not build an OS on the hardware. But I have not played with it, you are right.

    > TamaGo is a framework that enables compilation and execution of unencumbered Go applications on bare metal

    The environment does not seem to allow building a generic operating system [1]. F-Secure ported the runtime itself to boot natively. But please correct me.

    > There is no thread support

    The environment you run in is specifically curated for Go applications, such as the memory layout. I'd call this an "appliance" rather than enabling Go to be used for full-fledged generic operating system implementations.

    [1] https://github.com/f-secure-foundry/tamago/wiki/Internals

  • checkedc

    Checked C is an extension to C that lets programmers write C code that is guaranteed by the compiler to be type-safe. The goal is to let people easily make their existing C code type-safe and eliminate entire classes of errors. Checked C does not address use-after-free errors. This repo has a wiki for Checked C, sample code, the specification, and test code.

  • zz

    🍺🐙 ZetZ a zymbolic verifier and tranzpiler to bare metal C

    You're right that you can't define a safe subset of C without making it practical. MISRA C defines a C subset intended to help avoid C's footguns, but it still isn't actually a safe language. There are alternative approaches though:

    1. Compile a safe language to C (whether a new language or an existing one)

    2. Formal analysis of C, or of some practical subset of C, to prove the absence of undefined behaviour

    Work has been done on both approaches.

    ZZ compiles to C. [0] Dafny can compile to C++, but it seems that's not its primary target. [1][2]

    There are several projects on formal analysis of C. [3][4][5][6]

    [0] https://github.com/zetzit/zz

    [1] https://github.com/dafny-lang/dafny

    [2] https://dafny-lang.github.io/dafny/

    [3] https://frama-c.com/

    [4] https://www.microsoft.com/en-us/research/project/vcc-a-verif...

    [5] https://www.eschertech.com/products/ecv.php

    [6] https://trust-in-soft.com/

  • Scout APM

    Less time debugging, more time building. Scout APM allows you to find and fix performance issues with no hassle. Now with error monitoring and external services monitoring, Scout is a developer's best friend when it comes to application development.

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