Derek Jones (Unofficial) / Derek Jones (Unofficial) is on Nostr

Unofficial automated RSS/Atom links to Derek Jones's work on PASS (sample entries support the proposed topic). Original work is credited at the source; follow the source links. Zaps support the independent feed operator, not the author.

Last Notes

2026-11-02 03:55:08 GMT

Vote to adopt the C++26 draft as the new ISO standard fails
The vote to replace the ISO 2023 C++ Standard with an updated version has failed. Of the 28 P-member countries of SC22, 12 voted Approval, 8 voted Disapproval, and 8 Abstention. At least 66.66% of Approval votes are required (received 60%) and less than or equal 25% of Disapproval votes (received 41%), with Abstention votes not counting towards the total, and Disapproval votes by O-member countries counting towards Disapproval (there was one).
This post discusses the available courses of action over the next 12 months and then looks at factors influencing the continual evolution of the C++ Standard.
Some background for new readers. SC22/WG21, the ISO C++ committee, has been publishing new revisions of the C++ Standard on a 3-year schedule (i.e., 2011, 2014, 2017, 2020, and 2023), and until this setback was going to start work on 2029 at the next committee meeting. WG21 meet three times a year, with the week-long meetings attracting around 200+ people, who have a selection of 23 active subgroups to participate in. On average, there are 108 papers up for agenda time to discuss, and 147 post-meeting papers (average since 2024). This is industrial scale document processing.
What motivates 200+ people to regularly attend a gruelling week-long session of detailed technical C++ discussions? I have long said that the C++ committee has become a playground for bored consultants looking for a creative outlet. There are also the speakers and consultants who make their living talking about what’s new in C++, and giving training courses on the latest features of the language. The implementors are a tiny, but influential minority, because there are not many implementations. The energy driving WG21 comes from the people who attend. The bored consultants want their pet language feature adopted into the C++ standard, the speakers/consultants need something new to talk about, and the implementors need new features to be paid to implement (hopefully; funding is tough). WG21 is its attendee’s gravy train.
Nobody inside WG21 wants the gravy train to stop, so what happens next?
When a country votes Disapprove, they are required to specify what action the committee needs to take for them to change their vote to Approve. Removing contracts from the draft is what is required to turn the majority of Disapprove votes to Approve (various editorial issues were also requested by various countries). Contracts almost made it into the 2020 Standard, but was withdrawn at the last minute.
The WG21 committee has two options, and their next meeting starts in 2 weeks, 16th November, in Brazil:
agree to remove contracts, and vote to send the revised draft for another DIS (Draft International Standard) ballot at their March 2027 meeting (or June if the editorial work is not complete by March). The ISO directives specify that a second DIS ballot lasts 12 weeks, so the current draft minus contracts would be published around the third quarter of 2027, at the earliest. These directives also specify that a committee can only make changes that address Disapprove comments and cannot do any work revising a draft that is out for ballot.
The bored consultants have already spent almost a year sitting on their hands, while the current draft standard went through the (failed) approval process. Will they be willing to spend another year without their fix of C++ bike shedding?
skip to C++ 2029, i.e., not submit a contractless draft for voting, so C++ 2026/7 does not happen.
This immediately restarts the gravy train. If the supporters of contracts believe that the existing wording can be tweaked to make it broadly acceptable, they might not be willing to see it removed from the draft.
How contentious is the current specification of contracts? The 8 Abstentions is rather telling. Eight countries with people actively involved in WG21 work failed to reach consensus, including the US (the convention is for countries without active participation to be polite and vote Approve). Stroustrup, as a member of the US delegation, voted against the proposal, and has said (53 minute mark) “…it’s claimed to be a minimal viable product. It’s not minimal, it’s not viable.”
Contentious issues sometimes take many meetings to resolve. An extreme case is the 13-years before Fortran-77 became Fortran-90, with meetings described as “… two major vendors against the majority of X3J3 [ANSI Fortran committee] …”
One of the jobs of the chair of WG21, before forward a document for DIS balloting, is to be confident that consensus has been achieved. There was a change of committee chair at the start of this year. Even so, he is going to be in the hot seat at the next SC22 meeting.
What of the longer term future of work on the C++ Standard?
For some time I have been saying that WG21 is past its sell by date. The supporters of 3/4 industrial C++ compilers could meet together to agree new language features and their semantics, just like ECMAScript (aka JavaScript) and Java.
However, work on standards is controlled by those who do the work. If enough people continue to turn up at WG21 meetings and write papers, then the C++ Standard will continue to evolve. Cobol 2014 looked like it would be the final standard for the language, but as retirees like to say “I just had my eyes closed”, and we now have Cobol 2023 (the COBOL front end for gcc, which now supports COBOL 85).
The availability of LLMs creates two threats to established WG21 work practices, and a potential benefit.
The committee was straining under the volume of submitted papers, proposing changes, before LLMs arrived. Now that the effort needed to write and format a proposal has been significantly reduced, the number of papers submitted is likely to increase. While voting was underway, there were 116 papers in the May 2026 pre-Brno mailing, of which five acknowledge LLM assistance, thirty are very likely have had LLM assistance (according to Devin), and three possible uses of LLM,
the wording of the requirements in the C++ Standard has always been somewhat lax and open to interpretation (speaking as someone coming from a C Standards background, where there is a lot less ambiguity). Previously finding inconsistencies and ambiguities in the Standards’ document required a broad and deep understanding of that document. LLMs have removed the need for a broad/deep understanding of the language. If somebody were to decide to reduce the inconsistencies/ambiguities in the C++ Standard, they could use LLMs to submit a stream of issue requests, whose impact would be to overwhelm the current process, which currently has around 100 new issues added annually to the language issues list and around 250 added annually to the library issues list (averaged over the last few years),
coding agents provide a mechanism for removing a ball-and-chain that restrains all programming language committees (the compatible with C ball-and-chain was dropped in 2018). Compatibility with existing code, which conforms to the existing standard, is an oft cited reason for not changing existing behavior specified by the standard. Coding agents could significantly reduce the cost of updating existing code to handle changes to the semantics of C++. I’ll skip over the issue of how coding agents are trained on new language/library semantics, given that the only examples are contained in the proposal paper(s).
Given the expanding creative abilities of coding agents, the number of bored consultants is likely to grow. There will be a C++ 2032/3, whether the world wants/needs it or not.
https://shape-of-code.com/2026/11/01/vote-to-adopt-the-c26-draft-as-the-new-iso-standard-fails/
#iso #draft #internationalstandard #approve
#rss #feeds #linksharing #qwibbit

2026-10-26 03:38:53 GMT

Mutating Lean proofs looking for issues
A common technique used to bolster confidence that LLM derived proofs of mathematical statements are correct is to supply an associated machine checkable form of the proof written in the Lean language, i.e., a program that can be interpreted by the Lean proof assistant.
Mathematicians have discovered, shock horror, that LLM generated proof-programs contain bugs. Given the current trajectory of mathematical work, perhaps it should now be considered a field of software development (developers have long known that LLM generated code contains bugs).
Coding agents can generate programs that appear to work, while containing code having undesirable consequences (e.g., security issues) and surprising hallucinations, and it is only to be expected the generated Lean programs will contain these features. What can be done to check Lean programs for coding mistakes?
The traditional approach to finding issues with source is to read it. Lean proofs can contain many thousands of lines, and depending on your background be more/less easy to read than most programming languages. Reading Lean is the expensive, time-consuming, high value option. The source of an example Lean theorem is below:
theorem core_cycle (t : Nat → Nat) (h₀ : t 0 = 7) (h₁ : t 1 = 4) (h₂ : t 2 = 9)
(hp : ∀ n, t (n + 3) = t n) : t 2019 + t 2020 = 11 := by
have step : ∀ k, t (3 * k) = t 0 ∧ t (3 * k + 1) = t 1 := by
intro k
induction k with
| zero => simp
| succ k ih =>
have e1 : 3 * (k + 1) = 3 * k + 3 := by omega
have e2 : 3 * (k + 1) + 1 = (3 * k + 1) + 3 := by omega
constructor
· rw [e1, hp]
exact ih.1
· rw [e2, hp]
exact ih.2
have h2019 : 2019 = 3 * 673 := by decide
have h2020 : 2020 = 3 * 673 + 1 := by decide
have a : t 2019 = 7 := by
rw [h2019, (step 673).1, h₀]
have b : t 2020 = 4 := by
rw [h2020, (step 673).2, h₁]
rw [a, b]
One automated process that might be used to find suspect usage is mutation testing (which was once consigned to the grave). The idea is to mutate (e.g., make a non-trivial change) to the Lean source, and then check whether the mutated proof still validates. The assumption is that proof source that can be substantially mutated without changing its verification status is suspect.
Yesterday I took part in the Noetic X Nebius One Day Hackathon, and Team MutationHacker (Jacky Chen, yours truly, and Claude Open 5.5) worked towards creating a tool to automatically mutate and check Lean proofs.
Our grandiose plans were undermined by a submission deadline of 16:00 (we had around 5-hours). An agent based system that learned from past successful mutants was replaced by the MVP of a python program running on a laptop picking mutations at random and running the Lean verifier on the laptop (not fast). Successful mutants (i.e., no change to verification state) accumulated in the proof source.
How many mutants can a Lean proof of a theorem accumulate, and still verify, before it’s considered suspect or problematic? The mutation tool managed to add 13 mutants to the small test case that we used. I have no idea how representative this is.
The mutant generator specification lists of constructs not to use, e.g., changes that had no effect on the rest of the proof.
Perhaps the Lean source contains dead code, or bounding conditions are overly wide, e.g., can be replaced by .
lean-bugs is available on GitHub.
Ideally many thousands of mutants are tried, but the time taken to verify a short proof is several seconds, which will require lots of cpu time to check thousands of mutants. There don’t appear to be any benchmarks comparing Lean performance for various proof sizes (the timings cited don’t appear to connect to what I am after).
OpenAI’s recent Navier-Stokes solution came with 470K LOC of Lean which has been verified by independent researchers in times ranging from 212 seconds to 15 minutes. The smaller precursor theorems and lemmas could be mutated as stand-alone items, to reduce overheads.
https://shape-of-code.com/2026/10/25/mutating-lean-proofs-looking-for-issues/
https://shape-of-code.com/wp-content/plugins/wpmathpub/phpmathpublisher/img/math_995_c70e86b2715a6b83c6b5e6bbd59fdd56.png
https://shape-of-code.com/wp-content/plugins/wpmathpub/phpmathpublisher/img/math_995_9932c35cadd34be83d2ab994bf9de86a.png
#lean #leanproofs #mutatinglean #llm #nat #jackychen #dayhackathon
#rss #feeds #linksharing #qwibbit

2026-10-19 03:33:00 GMT

Program to extract x/y coordinates of points in pdf graphs
There are two techniques for specifying the display information contained in any graph within a pdf file. Raster graphics specifies (e.g., jpeg and png formats) the location and color of pixels, and vector graphics specifies (e.g., pdf and svg) the x/y coordinates of shapes/colors on the page. With vector graphics it’s possible to calculate the graph-axis relative positions of displayed symbols using the page relative x/y positions of each symbol (denoting a measurement point), the graph axis and axis tick marks/values; something I first did out in 2013. My Evidence-base software engineering book contains 10+ datasets that have been manually extracted from vector graphics within pdf files, i.e., by writing a graph specific awk script (a summary of the processes and tools used).
Can coding agents be used to implement a program detects and extracts the x/y coordinates (axis relative) of data points in any graphs, implemented using vector graphics, contained in a pdf file?
Do LLMs know of any tools that already do this? No.
This weekend I attended the Reinvent the Wheel: A Tools for Science Hack, where attendees were given credits for a month of Claude Max (these days I don’t write enough code to make it worth spending more than $20 per month on subscriptions). This was a perfect opportunity, and motivation, to create a specification of the data point x/y coordinate extraction process, and then to attempt to get a coding agent to generate a python program that extracted this data from any pdf file (whose plots were created using vector graphics).
Data points within a graph are drawn using a variety of symbols, and the symbols are drawn using a variety of techniques. For instances, a circle might be drawn using a single internal pdf instruction, drawing four quadrants using Bézier curves, or even eight Bézier curves, or who knows what (it’s very frustrating).
Then there are the tick marks along the axis, some of which are labelled with numeric values, don’t always start/finish at the ends of the axis, and denote a scale that could be linear or logarithmic.
My plan was to specify what was required, briefly describe the internal organization of a pdf file, provide a pdf file containing a single graph and the corresponding extracted data, as a csv file, and see what happens.
The start of my conversation with Claude Opus 5.5 follows:
Write a python program that takes as input a pdf file and
outputs the x/y coordinates of individual data points displayed
using vector graphics.
The vector graphics, as specified by internal pdf instructions,
used to display these data points appear on lines bracketed by
lines that just contain the words "stream" and "endstream"
The data points appear within a graph displayed on a page.
This graph contains an x and y axis and may contain other
unrelated lines and text within the plot's x/y axis.
The required x/y data point coordinates must be relative to
the values displayed on the plot's x and y axis.
Each x and y axis is drawn as one long line and short tick
marks for particular axis values.
An internal instruction is used to display a numeric value
close to its associated tick mark.
Various symbols may be used to display each data point.
For instance, in the attached pdf file a data point is denoted
by a circle created by joining four bezier curves.
The required x/y coordinate is at the center of the
approximate circle drawn by these four bezier curves.
All data point coordinates must be output, even data points
having the same x/y coordinates as other data points.
The attached file schump.tgz contains a pdf file and
a csv file containing the internal x/y positions of the
data points and the corresponding graph relative x/y positions,
it also contains the page number and the color of the data points.
Each graph is numbered.
It took about 15 minutes to create a python program that extracted the information from the pdf file that matched the contents of the csv file. I was impressed.
The generated program was then extended one feature at a time by describing some possible characteristics of a graph, and attaching a pdf containing a graph containing those characteristics; for instance (another 15-20 minutes):
Extend the program to support data points displayed as a
diamond shape created by drawing four lines.
The attached file 53cfc681e8e2afa9feb5820f4886e3018005-009.pdf
is a pdf file. The data points are denoted by diamonds created
by drawing four short lines.
This one/two feature at a time iteration looped six or so times before I grouped the remaining features into one update. Two+ hours later Claude provided 4K+ LOC of python code that appeared to handle everything.
The most impressive behavior was spotting minor issues that I had not mentioned and supporting them, or asking if they should be supported.
The pdfgraph2csv GitHub repo contains the code + regression tests.
Is the information in the output csv files correct?
The x/y coordinates of the points in the graphs in my book are available to be checked against. I also plan to repeat the process using a coding agent from another vendor, and to compare the contents of the corresponding csv files. N-version programming, here we come.
https://shape-of-code.com/2026/10/18/program-to-extract-x-y-coordinates-of-points-in-pdf-graphs/
#pdf #data #coordinates #program #tools #claude #sciencehack
#rss #feeds #linksharing #qwibbit

2026-10-16 03:14:39 GMT

Programming language choice is becoming a build option
What significant problems do high-level programming languages solve in a world of coding agents?
The original rationale for using high-level languages was to reduce the cost of porting existing software to different platforms. In a coding agent world, this is a benefit for those interested in having their software run on more than one platform. Is it a worthwhile benefit for those running on just iOS and Android (Shopify recently switched to a common codebase in React Native)? A general answer to this question will have to wait until things have settled down, some years from now.
Some software systems have configuration options that are selected at compile time. Having coding agents generate all possible option configurations is only practical when there are only a few possible combinations. The Linux kernel contains around 15,000 options, and while many of the possible option combinations are unrealistic, just 243,323 combinations produces a huge variety of executable programs. The source code approach is the only workable approach when many compiler time options need to be supported.
Existing practice is that program source code is written in a high level language, which is then translated to an executable form. Generating source in the programming language(s) being actively used enables coding agents to be seamlessly integrated into existing practices.
In specification based programming, English (or another human language) is the language used to create software. The actual programming language used when generating source code is not yet irrelevant.
Various kinds of activities are reviewed during the development of a software system. These include: requirements review, design review, code review, test review, and acceptance review.
Source code is needed for code review, which is frequently talked about but infrequently performed (an analysis of evidence; see section 6.6.1 for a summary of practices). Code review is a great mechanism for synchronizing practices within a team, training new developers and generally keeping team members up to date with what others are doing. These are benefits that apply when software is written by people. When source is generated by a coding agent, why do people need to review it? The reasons I have heard involve issues covered during requirements and design reviews. Another coding agent might check the code looking for mistakes, and this could be labelled as a (non-human) code review.
If the generated source is not going to be read by people, does it matter which programming language is used to generated it?
Coding agents require source code for training, and this is available in a variety of programming languages. Quantity of source code training data has a significant impact on LLM performance. Generating source in the language most likely to elicit the best coding agent performance is the obvious answer.
Choice of programming language is sometimes driven by current fashions, happenstance or a particular belief system. For instance, the conversion of existing non-Rust source to Rust is driven by the current fashionably status of that language, along with the effectiveness and low cost of coding agents.
Programming languages choice is evolving in to being a configuration option.
I’m sure that eventually somebody will convert the Linux kernel to Cobol and build a running system. As a start, I used the Devin coding agent to convert the contents of the kernel init directory to Cobol source and Fortran source. Both sets of source compile, but don’t link against any other kernel object files.
Before coding agents hackers were content to create their own new Linux distribution. To be leading edge in the future, a hacker will need to translate the Linux kernel and/or distribution to a language of their own creation (LLMs are now building compilers).
Single-handedly creating/implementing a language and using it to implement an operating system used to be a niche activity. First released in 2005, Terry A. Davis single-handedly wrote TempleOS in a language he created and implemented called HolyC, driven by a revelation from God. In the coming years, I expect to see many of these belief driven projects.
https://shape-of-code.com/2026/10/11/programming-language-choice-is-becoming-a-build-option/
https://shape-of-code.com/wp-content/plugins/wpmathpub/phpmathpublisher/img/math_994.5_afe5828673eab26ba3f519c30f04e4bc.png