C*: Unifying Programming and Verification in C

Posted by rramadass 6 hours ago

Counter64Comment38OpenOriginal

Comments

Comment by eggy 3 hours ago

I've been on this horse for a while now. I've settled on learning Ada/SPARK. Ada 2022 will start feeding a new SPARK 2014 update. Yes, they are both verbose, if you don't like that sort of thing, and don't like Pascal-like syntax. Believe me, I like APL/J/k/uiua/BQN and Forth and ASM. I am usually syntax agnostic as long as the PL and the ecosystem (more important than most think), meet your needs. I tried Rust back in 2018, and then again in 2023, but found it very complex and Ok, not a fan of the syntax. I would have preferred more ML or Haskell-like syntax. Zig seemed nice, but different use case, and too new. After all, Ada/SPARK have been on huge, high-assurance, high-safety applications for decades. Rust is getting some of their love, and vice versa. AdaCore had created a verified Rust compiler, but with a real world product (Blacktail hoist) in the works, we need a toolset and guarantees and ease of auditing and acceptance to achieve high safety and standards certifications. Think aerospace, defense, railway, and automotive. I started programming in 1977, so there's always a place in my heart for ASM/C. I played with F#, F*, and LOW from MS, and they are good, but they and Rust simply don't have the real world legacy of Ada/SPARK. I have been using Shen to write some formally verified models of less safety-critical areas of our software and I find it refreshing, however, my day job is to stay focused on Ada/SPARK until Rust matures more with a formally verifed proven toolset. There are certainly efforts and crates available in that direction, so hopefully others will bring it to where it needs to be. Lean is another one I have been playing with for some of the more overall logic proof of the system we are building.

Comment by pjmlp 1 hour ago

I think in 2026 complaining about verbosity is a moot point, when folks are programming writing book sized Markdown files for AI tools.

Heck, even complaining about COBOL programming feels like a joke now.

Kudos on you Ada adventures.

Comment by IsTom 35 minutes ago

I like the concept of separation logic as much as the next guy, but I don't think this is it. Just look at the examples, with loop invariants alone being longer than the whole example. It's not only a problem with ergonomics, but it leaves a lot of space for specification bugs.

And I suspect that cross section of people writing C code you want to verify with formal verification folks is not particularly big.

Comment by Jtsummers 24 minutes ago

> And I suspect that cross section of people writing C code you want to verify with formal verification folks is not particularly big.

Perhaps not, but C is still used in a lot of critical systems. Things like this for proving properties of some core of your program can be very helpful.

Comment by gavinray 5 hours 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...

Comment by UncleEntity 24 minutes ago

The problem I've been having is the LLM's are super dodgy, not even ten minutes ago the 'solution' to a proof failing was to disable that check in the static analysis harness so the tests pass since their first try (with a counter example and lemma from the literature in hand) didn't fix the issue.

Maybe it's an issue because it controls both sides of the fence and can change things willy-nilly when it thinks I'm just watching the youtubes but I haven't been able to find a another way to do this so, here we are...

Comment by rramadass 4 hours ago

The first thing people need to study is the "Correct by Construction" approach to programming as espoused by Edsger Dijkstra. Only then will the mathematical concepts used in verification aware languages start making sense and one can better understand what and how to use it.

One of the best books to learn this from is The Correctness-by-Construction Approach to Programming by Derrick Kourie and Bruce Watson - https://link.springer.com/book/10.1007/978-3-642-27919-5

The book actually uses Dijkstra's GCL language and wp-calculus along with Carroll Morgan's Refinement Calculus to demonstrate step-wise derivation of programs from specifications using a lot of examples.

Comment by Taikonerd 5 hours 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*.

Comment by slowcache 28 minutes ago

I think formal verification is a super interesting field, but this is a non-starter for me because I do not have a backwards E on my keyboard

Comment by gdwatson 5 hours 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.)

Comment by jensgk 5 hours ago

There already is a C* : https://en.wikipedia.org/wiki/C*

Comment by dymk 4 hours ago

That C* uses .cs, but nobody is complaining about C# using that extension

That C* was released in 1993

Who actually cares about the name collision?

Comment by mrkeen 3 hours ago

Found another one:

https://www.cs.columbia.edu/~sedwards/classes/2021/4115-fall...

https://github.com/kkysen/cstar

And to sibling comments: I care. Non-mainstream languages are talking points. I don't want to get 15 minutes into a "you should have effects like Koka" argument and then find out the other person is talking about a different Koka.

Comment by 4 hours ago

Comment by applfanboysbgon 4 hours ago

Does it matter? Is the global namespace permanently depleted because of an obscure language that nobody has used in 30 years?

Comment by stbenjam 3 hours ago

By that logic, I think I'll create a new language called Pascal, or maybe Ada...

Comment by Jtsummers 2 hours ago

Unlike the old C* linked at the top of this particular thread, Ada is still seeing active development in its language standard and implementations and new work. Pascal (via FreePascal and Delphi, in particular) is also still maintained and in use today.

Comment by applfanboysbgon 2 hours ago

Neither of those languages are obscure. If enough time passes that they become considered so, by all means there is no reason to condemn the names to an eternal graveyard.

Comment by rramadass 6 hours 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).

Note that the paper/language are from 2025 and so pretty recent.

Comment by 4 hours ago

Comment by glitchc 5 hours ago

Great idea, terrible syntax.

Comment by ahknight 5 hours ago

I say this about C every day.

Comment by ux266478 5 hours 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.

Comment by rramadass 5 hours 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 :-)

Comment by binaryturtle 5 hours 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. :)

Comment by ahknight 5 hours 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.

Comment by stvltvs 4 hours ago

Funny I think of Perl as Bash with slightly saner syntax plus robust regexp. (said with love)

Comment by hnlmorg 4 hours ago

The only thing Perl and C have in common is the curly-brace.

Comment by cwnyth 3 hours ago

I'm always surprised on here when I see others admin to liking C and Perl. It makes me feel less alone.

Comment by rramadass 4 hours ago

For me, C++ is always in first place. It allows me to do high-level abstractions to low-level hijinks all with total control (i.e. zero-cost abstractions, Templates for compile time programming etc.) across all levels of the software stack and the full spectrum of available hardware.

Furthermore, any C++ programmer who says they do not know C, knows neither C nor C++ (hence my preference in using C/C++ as a shorthand to encompass both and highlight the dependency of the latter on the former). I often see this in novice C++ programmers who started with "Modern C++" and identify it as something like Java/C# because of the now huge set of standard libraries and copious syntactic sugar which only compounds their confusion further.

Comment by applfanboysbgon 4 hours ago

> Furthermore, any C++ programmer who says they do not know C, knows neither C nor C++ (hence my preference in using C/C++ as a shorthand to encompass both and highlight the dependency of the latter on the former).

Right, but this dependency is one-way. There is an entire legion of C programmers who reject C++ (most notably Linus), so claiming that almost all C programmers are also C++ programmers is a bit off.

Comment by rramadass 3 hours ago

What i meant was that almost all C programmers are aware of and know C++ to varying degrees. But they choose to not use it for their application based on needs/expertise/etc.

Linus Torvalds objection to using C++ is perfectly logical for his use-case. I know many embedded programmers who refuse to use C++ even though they understand and agree with the benefits that it can bring to the table. Their C expertise is so good that when they program, cognitively the language just disappears and they "flow" through the problem solution implementation. This is the crux of problem-solving.

Comment by EPWN3D 2 hours ago

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

This is... not true at all.

Comment by theokrueger 5 hours 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.

Comment by ux266478 4 hours ago

And neither can be made as ergonomic as no verification at all. It's all about how much you need. Functional verification isn't an appropriate tool where a single bug is catastrophic.

> yet nothing prevents you or your agent from changing invariants to fit the algorithm and making it incorrect.

If the thing we're trying to prove is ungrounded, it's trivially true that any verification method falls apart. You're still encoding priors in your testing methodology. No matter how robust you think your testing suite is, I can still trick it if given free reign over the codebase.

Comment by bellowsgulch 4 hours ago

I suspect that there is a body of C programmers out here that use C on a regular basis that aren’t posting who know that using C safely is 99% just using Valgrind and some specific GCC or llvm flags and you’re done.

They don’t reply to these threads to share that knowledge because these threads devolve into cesspools about how you should just use Rust despite the language not meeting specific requirements authors have that you have to do additional work and maintenance for in “safe” languages that you get for free in C because you don’t have to emulate it.

Comment by AlotOfReading 49 minutes ago

    using C safely is 99% just using Valgrind and some specific GCC or llvm flags and you’re done
I wish that were the case, but it's not. Dynamic analyzers are fantastic and everyone should be using them constantly, but they don't solve the problem of UB. They tell you whether your code, as translated by a specific compiler using a specific set of flags today has detectable problems. There are still gaps, and what's true today might not be true even for the same source code built tomorrow, or given different inputs. Asserting my safety-critical code does X or Y is important to me, and neither C nor C++ have standard tooling that fully addresses that need.

Other languages are much farther along than this. You can in theory take a pile of Rust and isolate exactly the points where undefined behavior might occur, or eliminate them entirely in Ada/Spark.

Comment by Jtsummers 4 hours ago

> I suspect that there is a body of C programmers out here that use C on a regular basis that aren’t posting who know that using C safely is 99% just using Valgrind and some specific GCC or llvm flags and you’re done.

C* (the submitted language) is not just about determining memory correctness and related program features like what Valgrind will do for you (or help with). It's about proving correctness of programs more generally, so any C programmer not looking at it because they know about Valgrind are choosing to skip something interesting for a very poor reason.

Comment by rramadass 4 hours ago

> I suspect that there is a body of C programmers out here that use C on a regular basis that aren’t posting who know that using C safely is 99% just using Valgrind and some specific GCC or llvm flags and you’re done.

Absolutely right! I sincerely hope they share their knowledge here and elsewhere.

> They don’t reply to these threads to share that knowledge because these threads devolve into cesspools

HN is often rage-inducing when it comes to comments on C/C++/Fortran/Cobol/etc. older languages and systems. There are many critical and industrial-strength systems developed by the previous generation of engineers/programmers which today's noobs/cargo-cultists cannot even hope to imagine much less understand.

As an example, people talk about all the great features provided by Erlang but forget that its BEAM VM where most of the "magic" resides is actually written in C! Imagine how much expertise lies buried in its implementation!