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.
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.
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...
I totally agree. I have this nagging feeling that LLMs push things like this past the breaking point. Effects and contracts are _obviously_ useful to humans as well, we've just gotten by without them for a long time. But when you have intelligence on demand, context building is a huge bottleneck, and local reasoning becomes way more useful from an efficiency perspective.
I'd love to see some actual experiments with LLMs in this area. There are a fair number of languages with effect implementations at this point.
I've been looking at model checkers and program proof assistants on and off since FDR and Isabelle/HOL and the like, and there were similar tools going back another decade before that. If you're verifying part of an ASIC or a crypto protocol or something similar they're fine (if extraordinarily painful to use), but for anything else they've been bypassed by AI. I'm not saying that as an AI fan but because by the time you get your PhD and then spend another five years learning how to use the tool and mark up the code and hope you got the markup right and after another six months of what feels like trying to make a string go in a certain direction by pushing it and the tool finally finds a nonexploitable buffer overflow in a function that's never called you realise you could have done the same thing with $2 in AI tokens. It's the program verification technology of the future, and always will be, while "claude, find places where this code does things it shouldn't" is right now and doesn't require a PhD to use.
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.
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.
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.)
> 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!
That is called Trusted Computing Base in security speech, having ensure Erlang runtime implementation is safe, is a much reduced effort than certifying a telecommunications distributed application 100% written in C as equally safe under the same attack vectors.
Security Standards/Frameworks like "TCB" (https://en.wikipedia.org/wiki/Trusted_computing_base), "Common Criteria" (https://en.wikipedia.org/wiki/Common_Criteria) etc. are not what i am talking about here. I am pointing to the fact that there is a large piece of industrial-strength C code (i.e. BEAM/ERTS) whose architecture/complexity/techniques are manifested as the "features" of another higher-level language (i.e. Erlang). People seem to appreciate the latter while not comprehending the former. The underlying C-based infrastructure is so good that there are now multiple different-paradigm languages targeting the BEAM.
Incidentally, the C implementation of BEAM/ERTS is not formally verified; only some parts of the upper-layer intermediate representation and bytecode have been verified. Also an Erlang distributed cluster was designed to operate only within an already secure network (i.e. telephone network) and not on today's public Internet. So if you want to run Erlang securely you would need to know overall system security architectures and follow advice given by the "Erlang Ecosystem Foundation Security Working Group" - https://security.erlef.org/
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.
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.
I started recently to learn Cobol, since 2 companies my friend and son were working at need them desperately. They would prefer people with experience in the bankiing/finance industry, but at this point all the over 60s guys are leaving, and nobody is left to pick up the mantle. They told me even though the money is great >$225k starting, people don't want to maintain legacy Cobol code with very high risk if you mess up.
The language is actually relatively modern, it kept up with time (latest ISO version is from 2023), and there are even IDEs like Rocket Visual COBOL, granted not something that you might get on e.g. z/OS, but there are others.
It actually compiles to native code, it handles well its use case, batch processing business data, and despite everything less verbose than most agents markdown files I keep seeing.
Yes the risk is there, but it is also there for any kind of legacy application in enterprise scenarios, which is why most migrations fail.
I'll have to dive back in. I could use the decent salary right now. I've been out of work aside from my endeavors to bring this hoist to market we are working on currently. The whole formal verification thing has become an obsession of mine lately. First it was applied to just the safety-critical aspects of our system. Now, I am applying lesser, but still powerful methods and tools to make sure the whole front end and basic networking is also part of this formal verification chain. Down the rabbit hole!
Refactoring legacy code seems like something where formal methods could help. "Prove that these 2 subroutines are equivalent, across all inputs" is exactly the kind of thing that they're good at!
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.
As of 2024, ATS/Xanadu (ATS3) is being developed actively in ATS2, with the hope of reducing the learning needed by two main improvements:
- Adding an extra layer to ATS2 to support ML-like algebraic type-checking
- Type-based metaprogramming using algebraic types only
With these improvements, Xi hopes for ATS to become much more accessible and easier to learn. The main goal of ATS3 is to transform ATS from a language mainly used for research, into one strong enough for large-scale industrial software development.
> We claim that C achieves real-time program verification, i.e., the user can carry out verification
as they program the implementation code incrementally. It achieves this goal by orchestrating the
symbolic-execution engine and the LCF-style proof kernel together, creating a proof-supporting
runtime that runs proof-code blocks and symbolic execution of program segments in an interleaving
manner
That's why such thing is mostly useless. C is used in places where performance is important and nobody want to sacrifice performance for such proofing. Even more, if such proofing is too slow, it's better to use something like Fil-C.
40 comments
[ 0.29 ms ] story [ 70.5 ms ] threadF* is in the ML family of languages, so it looks pretty different from C*.
Wrote a bit about this recently
https://gavinray97.github.io/blog/design-by-contract-and-eff...
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.
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...
Also see resources at https://news.ycombinator.com/item?id=49269323
I'd love to see some actual experiments with LLMs in this area. There are a fair number of languages with effect implementations at this point.
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.
> 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://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.
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.
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!
Incidentally, the C implementation of BEAM/ERTS is not formally verified; only some parts of the upper-layer intermediate representation and bytecode have been verified. Also an Erlang distributed cluster was designed to operate only within an already secure network (i.e. telephone network) and not on today's public Internet. So if you want to run Erlang securely you would need to know overall system security architectures and follow advice given by the "Erlang Ecosystem Foundation Security Working Group" - https://security.erlef.org/
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.
Heck, even complaining about COBOL programming feels like a joke now.
Kudos on you Ada adventures.
It actually compiles to native code, it handles well its use case, batch processing business data, and despite everything less verbose than most agents markdown files I keep seeing.
Yes the risk is there, but it is also there for any kind of legacy application in enterprise scenarios, which is why most migrations fail.
Also see Round-Trip Correctness: A New Metric for Generative AI-Based Process Modeling - https://news.ycombinator.com/item?id=49033317
And I suspect that cross section of people writing C code you want to verify with formal verification folks is not particularly big.
The ATS Programming Language - https://www.cs.bu.edu/~hwxi/atslangweb/
ATS3-Xanadu - https://github.com/githwxi/ATS-Xanadu
From https://en.wikipedia.org/wiki/ATS_(programming_language)
As of 2024, ATS/Xanadu (ATS3) is being developed actively in ATS2, with the hope of reducing the learning needed by two main improvements:
- Adding an extra layer to ATS2 to support ML-like algebraic type-checking
- Type-based metaprogramming using algebraic types only
With these improvements, Xi hopes for ATS to become much more accessible and easier to learn. The main goal of ATS3 is to transform ATS from a language mainly used for research, into one strong enough for large-scale industrial software development.
That's why such thing is mostly useless. C is used in places where performance is important and nobody want to sacrifice performance for such proofing. Even more, if such proofing is too slow, it's better to use something like Fil-C.