The author includes a footnotes for "BUT RUST.." and "BUT ZIG..", but how about Nim? Looks like there is a native library implementation of `lowerBound` https://github.com/nim-lang/Nim/blob/version-2-0/lib/pure/al... Yes, it's not a "bare-metal" language, but it compiles to one (or two), so it would be interesting to see what it compiles to here.
Also, what's wrong with C?
Zig’s binary search is here, it’s an unoptimized textbook version: https://github.com/ziglang/zig/blob/b835fd90cef1447904d3b009...
At TigerBeetle, we have our own branchless implementation here:
https://github.com/tigerbeetle/tigerbeetle/blob/e996abcf7154...
How much faster is the branchless version in practice? I make heavy use of binary search in some code I maintain, and I wonder if it would make much of a difference to switch to a more efficient version of the function.
I see (left+right)/2. Is it like python with unbounded precision?
Where do you see that in the code? I can't see (left+right)/2 anywhere in the code I linked?
No, it uses 2’s complement and is well defined in release mode. From [1]:
> When you’re compiling in release mode with the --release flag, Rust does not include checks for integer overflow that cause panics. Instead, if overflow occurs, Rust performs two’s complement wrapping.
[1]: https://doc.rust-lang.org/book/ch03-02-data-types.html#integ...
This array would not fit in any kind of memory for the foreseeable future :)
https://doc.rust-lang.org/nightly/rustc/platform-support.htm...
[1]: https://doc.rust-lang.org/stable/reference/types/numeric.htm...
There is no (left+right)/2 on that page.
let mid = left + size / 2;
old branchless version: https://github.com/rust-lang/rust/pull/45333/files
Oodles and oodles of undefined behaviour, for example.
C ain't clean.
All I know is that it tries to ensure that the behavior of the program is the same as the input, meaning that the compiler itself does not have bugs. But how does that actually interact with undefined behavior in the language? What happens to an array out of bounds?
And what are the limitations imposed, since it only works on a subset of the C language?
It seems unlikely that I could just switch compilers and suddenly have a safe program written in C.
> Third, the compiler is allowed to improve the behavior of the source program. Here, to improve means to convert a run-time error (such as crashing on an integer division by zero) into a more defined behavior. This can happen if the run-time error (e.g. division by zero) was optimized away (e.g. removed because the result of the division is unused). However, if the source program is known to be free of run-time errors, perhaps because it was verified using static analyzers or deductive program provers, improvement as described above never takes place, and the generated code behaves exactly as one of the allowed behaviors of the source program.
So you still have to prove your program's correctness by some other means.
For CompCert, the high-level correctness theorems I proved are all of the first kind above: if the source program goes wrong, nothing is guaranteed about the behavior of the compiled code. It happens, however, that the stepwise simulation lemmas I build on actually prove property 2 above: the compiled code cannot crash "earlier" than the source code, and will produce the same pre-crash observables, then possibly more. So maybe I should strengthen my high-level correctness theorems...
But yes, mechanically proving additional properties with some kind of SAT solver is also an open area of research. Dafny is the example I’m familiar with. Its conditions and invariants allow things like automatically proved binary search[2]. Converting CompCert C statements to SMTLibv2 assertions (which is, to an extremely rough first approximation what Dafny does) would certainly be considerably easier than it would be for most other languages. It would still be a serious effort of course.
[1] https://blog.regehr.org/archives/232
[2] https://github.com/dafny-lang/dafny/blob/master/Test/dafny4/...
> In portable C code I/O is performed using function calls of the standard library. A compiler can generally not assume that a function returns to the caller, because the function could call ‘exit’, ‘abort’, ‘longjmp’, or enter an infinite loop. For this reason, it is never allowed for a compiler to use any information derived from an operation with potential UB that comes after a function call in a way that could affect observable behavior before the function call. Consequently, observable behavior that is accessed via function calls (i.e. all except volatile accesses) can not be affected by time-traveling optimizations even when using the abstract interpretation. In principle, a compiler could use special knowledge about C library functions and use the fact those functions always return to the caller, but we are not aware of any compiler which does this (and it hardly seems worthwhile).
I believe LLVM has a "mustreturn" attribute expressing this, but as noted, no standard C library messes with any such attributes for functions that cause observable behavior.
So time-traveling UB really only affects programs which use volatile accesses for MMIO, and it might eventually be banned entirely from the C standard if the linked proposal N3128 goes through. I'd say that even "some C bugs" is a overstatement outside of embedded programming, given the rarity of MMIO in a hosted environment.
[0] https://www.open-std.org/jtc1/sc22/wg14/www/docs/n3128.pdf
I don’t concede your claims, but I’m enough out of the loop that I won’t attempt to refute them either. However, for what it’s worth, embedded programming is exactly where I most want that.
Furthermore, I don’t know of any other popular bare metal language that’s even close to having a compiler offering mechanically provable assertions about its compiled behavior. Do you?
You can automatically extract low level code out of certain high level, provable languages. I think some of them might offer the guarantee you asked for (assuming you eg use a certified C compiler for the last leg).
Well, if you ask the question that narrowly, then I suppose not, unless CakeML's GC is lightweight enough to be stuffed onto some board or another.
But 99% of the time (i.e., when I am not doing something intentionally strange to test the language's limits), the correctness of the program I'm writing, or at least of its dependencies (including the standard library), is far more questionable than the correctness of the compiler; after all, the output of, say, GCC and LLVM has been tested by oodles of real-world software. Even if I'm really paranoid, I can disable all optimizations and reenable any less-questionable ones individually.
Thus the GP's complaint, that C is filled to the brim with undefined behavior that will silently cause corruption in production code instead of failing loudly, since all the runtime sanitizers (AFAIK) swear up and down that they aren't very secure.
I do hope that that formal verification on the program's side becomes more accessible in the future, though, either via dedicated systems like Daphny or via "gradual verification" as permitted by things like Why3 frontends for different languages. (In particular, I've been meaning to look into the Creusot project for Rust.) But short of formal verification, robust runtime assertions and guardrails are generally the best bet, and C as a language simply doesn't provide very good tools for those.
That's helpful, but doesn't make the language itself saner.