C*: Unifying Programming and Verification in C

(arxiv.org)

21 points | by rramadass 1 hour ago

7 comments

  • gdwatson 1 minute ago
    Names for C successor languages are pretty well exhausted by this point, so I sympathize, but I strongly associate the name C* with a decade-old rant about C compilers’ aggressive exploitation of undefined behavior: https://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_20... . (In calling it a rant I don’t mean that it’s altogether unpersuasive. Its style is just a bit spicier than I am used to seeing typeset in Computer Modern.)
  • jensgk 4 minutes ago
    There already is a C* : https://en.wikipedia.org/wiki/C*
  • gavinray 28 minutes ago
    I really think that verification aware languages are going to become a necessity

    Wrote a bit about this recently

    https://gavinray97.github.io/blog/design-by-contract-and-eff...

  • Taikonerd 31 minutes ago
    The authors cite this, but just to mention it: this sounds like F*, another proof-oriented language. (https://fstar-lang.org/)

    F* is in the ML family of languages, so it looks pretty different from C*.

  • theokrueger 16 minutes ago
    formal verification is great and all, but you can never make it as ergonomic as functional verification. this matters for agents and real people alike.

    formal verification requires a deeper understanding of underlying mechanisms to write correctly. yet nothing prevents you or your agent from changing invariants to fit the algorithm and making it incorrect.

  • rramadass 1 hour ago
    The "C*" language website - https://cstarlang.org/en/intro.html

    See in particular, usage benefits with LLMs (last para of https://cstarlang.org/en/intro.html) and how to use it with LLMs (https://cstarlang.org/en/tutorial/cstar-mcp.html).

  • glitchc 51 minutes ago
    Great idea, terrible syntax.
    • ux266478 6 minutes ago
      Yeah I dislike it. Why are we babyducking sepples attributes? And what I assume to be namespace accessors? Why are logical assertions enclosed in backticks? I "get it", because it's actually kind of difficult to make a backwards compatible derivative of C that doesn't devolve into glyph soup, but this has a massive frankengrammar stink to it. The proof language is eyebrow raising to say the least.
    • ahknight 26 minutes ago
      I say this about C every day.
    • rramadass 39 minutes ago
      What's terrible about the syntax? Using "[[require/ensure/invariant/proof/assert/etc.]]" is actually pretty neat.

      And given that almost all C programmers are also C++ programmers, no mere syntax can faze us :-)

      • binaryturtle 28 minutes ago
        In my own ranking of favourite programming languages C is at the first place. C++ comes in last. I personally hate it when people write C/C++ as if it's the very same thing. I'm quite sure there's more like me out there. :)

        Interestingly Perl comes in second, even I use it rarely (aka not at all) these days. But that's a slightly off-topic side note. :)

        • ahknight 19 minutes ago
          Perl is just C with less type safety.

          And yes, for the most part. C++ as simple shorthand for struct-attached functions and automatic memory management (no, not smart pointers; RAAI) is good. Every single thing added after that is misery and should push a modern developer to Rust, Go, or Zig (roughly in that order) where such things are implemented sanely or not at all.

          • stvltvs 0 minutes ago
            Funny I think of Perl as Bash with slightly saner syntax plus robust regexp. (said with love)