checkedc VS zz

https://github.com/microsoft/checkedc

Also, one can combine subsets of C with FOSS, static analyzers that can handle those subsets. Then, compose only in ways that the tools can handle. Then, combinatorial and fuzz testing of the interface composition.

I know you’re doing the project for fun while exploring specific ways to achieve your goals. So, these are just some links and concepts that might help on your journey. Lots of folks don’t know about prior work in this area. So, I keep passing it on.

- [Checked C](https://github.com/microsoft/checkedc) - extensions to make C safer #cpp

Yes. Microsoft Research is working on "Checked C": https://www.microsoft.com/en-us/research/project/checked-c/

As a test, someone ported FreeBSD's networking stack to Checked C. It was easy and there was no overhead to performance and binary size.

Haha. I think they did ultimately agree. Thus a later research project is: Checked-C

There is this: https://github.com/zetzit/zz

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/

Formal methods have been used successfully for decades; it's not just a pipe dream. Perfect software should ideally be something like ultra-low-defect software, though (that's the term the AdaCore folks use).

There are also other projects that aim to make formal software development much easier [0][1] and of course there's SPARK Ada.

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

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

This post reminds me that I've been wanting to try out ZetZ[0]. It incorporates Z3 into a high-level programming language, and seems to do a lot of what the post talks about automatically.

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

I still want to try the ZZ language (https://github.com/zetzit/zz) someday. It compiles to C, and uses a SMT solver to prove that you don't index out-of-bounds at compile time. But I don't like how it lacks generics, uses C idioms, and compiles to C.

The zz language uses a SMT solver to check for program soundness... I haven't tried it, but that's got to be more flexible and resource-hungry.

Especially the fact that it outputs C code. So interop is seamless.

https://github.com/zetzit/zz

For any systems language, interop with C is the litmus test.

With that in mind, this new language should not require 15,000 lines of standard library. A type-safe wrapper for libc should be enough...

You might find ZetZ interesting!