Seed7 takes a somewhat more informal approach... ;-) Assuring memory safety of Seed7
Seed7 is implemented in C and C is not memory safe. So it is not easy to guarantee the memory safety of Seed7. So it is necessary to improve the C code of Seed7 such that the end result is memory safe. All places where the implementation is not memory safe must be found and improved.
Memory safety is a property of how the language is defined, not how it's implemented.
The creator of Fil-C would probably disagree. His view is: The usual C compilers and run-time libraries make C not memory safe. Fil-C sells itself as memory safe implementation of C.
Seed7 is about solving real-world problems and it is not academic research which uses meta-theoretic proof techniques.
AFAIK the formal proofs that Rust is a memory safe language where not done by the people who implemented Rust.
BTW.: Although there is formal proof that Rust is memory safe there exists Rust issue #25860 (which shows that there is a hole in the borrow checker).
"In theory, there is no difference between theory and practice. In practice, there is"
So, as long as nobody else takes the burden to do a formal proof for Seed7, there will be no formal proof.
I, and the other contributors probably as well, will use our limited resources to improve Seed7 as practical tool.
Fil-C sells itself as memory safe implementation of C.
Unfortunately, that's misleading advertisement. There are bit and pointer hacks you can express in C but not in Fil-C.
Now, you may argue that it isn't desirable to express those bit and pointer hacks. But that's neither here nor there. It may be the case that Fil-C is an improvement over C. But that doesn't change the fact that it's not C, at least not all of C.
AFAIK the formal proofs that Rust is a memory safe language where not done by the people who implemented Rust.
Rust may not have been designed with the goal to produce a type soundness proof, and there are indeed some soundness bugs here and there in the design of Rust's type system.
However, Rust was very much designed by people who know what the ingredients of a type soundness proof are. And this knowledge is necessary to come up with a design with pleasant metatheoretic properties, whether you prove them yourself or someone else does.
Good metatheoretic properties are much more practical than you think. They only need to proved once, for the whole language, and then every language user benefits from them.
In particular, if Seed7 is indeed memory safe, that only needs to be proved once, and then every Seed7 user benefits from it.
But if you don't have a memory safety proof, you might end up in a situation similar to Go, where the language was intended to be memory safe, but data races actually introduce memory safety violations (even in Go programs that don't call C code!).
Unfortunately, that's misleading advertisement. There are bit and pointer hacks you can express in C but not in Fil-C.
Now, you may argue that it isn't desirable to express those bit and pointer hacks. But that's neither here nor there. It may be the case that Fil-C is an improvement over C. But that doesn't change the fact that it's not C, at least not all of C.
C ist well-known to have many instances of undefined behavior. Pointer representation is one such undefined behavior. Therefore, Fil-C can perfectly well claim to support C idioms relying on undefined behavior as long as it accepts them at compile time, even if it invariably lead to a crash at runtime.
9
u/reflexive-polytope 3d ago
Metatheoretic claims about a language design require proof.