[HN Gopher] Why the C Language Will Never Stop You from Making M...
       ___________________________________________________________________
        
       Why the C Language Will Never Stop You from Making Mistakes
        
       Author : zaphar
       Score  : 30 points
       Date   : 2021-12-30 14:53 UTC (8 hours ago)
        
 (HTM) web link (thephd.dev)
 (TXT) w3m dump (thephd.dev)
        
       | spacechild1 wrote:
       | Off topic, but this is the author of my favourite Lua C++ binding
       | library (https://github.com/ThePhD/sol2). Great guy!
        
       | DerekL wrote:
       | Dupe: https://news.ycombinator.com/item?id=29728594
        
       | dandotway wrote:
       | Frama-C allows writing formally verified bug-free C. It is
       | certainly tedious though; you essentially have to write two
       | versions of every function: (1.) the actual C code for the
       | function; (2.) a declarative formal specification of what the
       | function does in ACSL (ANSI C Specification Language), stating
       | all relevant pre-conditions that must be met prior to calling the
       | function, and all relevant post-conditions that hold after the
       | function runs. Then you have to add annotations to computation
       | steps in the function code proving it causes the post-conditions
       | to hold if the pre-conditions hold.
       | 
       | Nevertheless, it is extremely powerful because it can prove the
       | correctness of arbitrary heap manipulation algorithms (lists,
       | trees, graphs). You can formally prove complicated C pointer
       | manipulations are correct that cannot be expressed in 'safe
       | Rust'. There is also the CompCert formally verified C compiler.
       | 
       | I've also studied Ada/Spark's formal verification abilities and C
       | is way ahead here. C is also way ahead of C++ because C has far
       | fewer complicated semantic rules that need to be formalized
       | before they can be analyzed. Even parsing C++ is an enormous
       | task.
       | 
       | In the coming decades as the automation and ease-of-use of formal
       | verification tools improves, I think C may well end up being the
       | best choice for security-critical and correctness-critical
       | systems programming. With current tools it is already ahead of
       | Ada, C++, and Rust.
       | 
       | https://frama-c.com/
        
         | joe_guy wrote:
         | Thank you for the write up. I'll be reading up on this more.
         | 
         | Do you know if it models the target arch, too? Like, can it
         | account for different architectures having different
         | instruction reordering rules?
        
           | dandotway wrote:
           | Frama-C doesn't need to know anything about the target arch.
           | It guarantees no undefined / implementation defined behavior
           | on _all_ architectures. You have to prove your code does not
           | cause overflow /underflow (or accounts for it) if you add two
           | integers or cast a uint32_t to an int32_t, etc. Very tedious,
           | but it can and is being done.
           | 
           | CompCert, the formally verified C compiler, is a separate
           | thing from Frama-C, but currently supports x86, ARM, RISC-V,
           | and PowerPC. (CompCert is actually mostly programmed in OCaml
           | and the Coq/Gallina proof assistant.) CompCert guarantees
           | that a correct ISO C program (no undefined or implementation
           | defined behavior) is translated into an assembler program
           | with the same semantics, i.e. an assembler program that
           | computes the same results as the C source program. So
           | CompCert for each supported architecture needs a formal
           | semantics for any CPU instructions it generates. CompCert is
           | an optimizing compiler and the optimizer accounts for the
           | delay between when an instruction is issued and when the
           | result is ready, accounts for pipelining and all that if that
           | is what you are asking.
           | 
           | But to write verified C programs you don't need to worry
           | about instruction re-ordering happening lower down changing
           | the meaning of your program and all that. That's a deeper
           | layer of the onion, and, as Bjarne Stroustrup said, each time
           | you peel a layer of the onion you cry more.
        
       ___________________________________________________________________
       (page generated 2021-12-30 23:01 UTC)