C*: Unifying Programming and Verification in C

gdwatson 11 minutes ago | parent | next [-]

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.)

▲

gavinray 38 minutes ago | parent | prev | next [-]

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...

▲

jensgk 14 minutes ago | parent | prev | next [-]

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

	▲	dymk 6 minutes ago \| parent \| next [-]
		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?
	▲	applfanboysbgon 6 minutes ago \| parent \| prev [-]
		Does it matter? Is the global namespace permanently depleted because of an obscure language that nobody has used in 30 years?

▲

Taikonerd 41 minutes ago | parent | prev | next [-]

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 26 minutes ago | parent | prev | next [-]

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.

▲

bellowsgulch 6 minutes ago | parent | prev | next [-]

[delayed]

▲

rramadass an hour ago | parent | prev | next [-]

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.

▲

glitchc an hour ago | parent | prev [-]

Great idea, terrible syntax.

▲

ux266478 16 minutes ago | parent | next [-]

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 36 minutes ago | parent | prev | next [-]

I say this about C every day.

▲

rramadass an hour ago | parent | prev [-]

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 38 minutes ago | parent [-]

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 29 minutes ago | parent | next [-]

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.

	▲	hnlmorg 4 minutes ago \| parent \| next [-]
		The only thing Perl and C have in common is the curly-brace.
	▲	stvltvs 10 minutes ago \| parent \| prev [-]
		Funny I think of Perl as Bash with slightly saner syntax plus robust regexp. (said with love)

▲

rramadass 9 minutes ago | parent | prev [-]

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.