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.
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.
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.)
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.
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.
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.
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. :)
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.
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.
> 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.
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.
> 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.
> 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!
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...
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.
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.)
There already is a C* : https://en.wikipedia.org/wiki/C*
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?
Does it matter? Is the global namespace permanently depleted because of an obscure language that nobody has used in 30 years?
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*.
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.
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.
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.
https://news.ycombinator.com/item?id=49613696
Great idea, terrible syntax.
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.
I say this about C every day.
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 :-)
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. :)
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.
Funny I think of Perl as Bash with slightly saner syntax plus robust regexp. (said with love)
The only thing Perl and C have in common is the curly-brace.
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.
> 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.
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.
> 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.
> 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!