zz VS BorrowScript

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!

You might be looking for something like https://github.com/alshdavid/BorrowScript

I think AssemblyScript is the best example.

Adding the borrow checker is quite invasive though. This guy is trying https://github.com/alshdavid/BorrowScript.

I think it's a kind of fun constraint that experienced and bored devs like to challenge themselves with - the borrow checker. The latest obsession. You absolutely don't need a borrow checker, just like you didn't need everything to be functional programming, but it's intellectually stimulating.

Sounds like BorrowScript, which is TypeScript syntax, a Rust borrow checker, and Go-like coroutines. It's designed for wasm and web api targets. (not compatible with TypeScript though)

https://github.com/alshdavid/BorrowScript

I asked how to implement a "borrow checker" in JavaScript in my initial attempts (I've learned a decent amount since), which led me to randomly finding BorrowScript that seems to have another implementation I think, so going to be taking a deeper look there for inspiration as well. But if one could explain the steps of the algorithm, and how it integrates/relates with the type inference process, that would be of great use. Not for learning how to use Rust, but to learn how this aspect of its compiler works.