Permalink
Reply
On Thursday, 17 June 2021 at 09:56:52 UTC, Alexandru Ermicioi wrote:
>C has no verification, and what is the result of this? Lot's and lots of bugs due to human errors.
True, although there are dialects of C that have more advanced verification than D, both research projects and industrial projects.
>One more thing for verification to be present, is that it saves me time. I don't have to be extra careful while writing code, and certainly won't need to spend more time debugging a bug that could be prevented by automatic code verification.
Indeed. But if you think about C functions that require arrays of zero terminated strings… Ok, you can create a simple @trusted wrapper, but then that wrapper has to check that all the strings are zero terminated, which adds unacceptable overhead. So even in this trivial example the @trusted code has to assume that the provided data structure is correct, and thus it enables @safe code to make correct @trusted code unsafe.
It gets even more complicated in real system level programming where you might make a function @trusted because you know that when this function is called no other threads are running. That is an assumption about an invariant bound to time.
Proving things about timelines and concurrency is difficult/impossible. So, in practice, the correctness of @trusted is ad hoc, cannot be assumed to be local and requires audits as the code base changes.
But it could be helpful to list the invariants unsafe code depends on, e.g.:
@unsafe(assumes_singlethreaded){
…fast update of shared datastructure…
}
@unsafe(pointer_packing, pointer_arithmetics){
…
}
@unsafe(innocent_compiler_workaround){
…
}
Now you have something to scan for. Like, in testing you could inject a check before the code that assumes no threads to be running. If you build with GC then you can scan all used libraries that does tricks with pointers and so on.
For true system level programming something like this (or more advanced) is needed for people to use it. Otherwise just slapping @system on all the code is the easier option. There has to be some significant benefits if you want programmers to add visual noise to their codebase.
You could also add a tag that says when the unsafe code was last audited (or at all):
@unsafe(pointer_arithmetics, 2021-06-17){
…
}
