At a Stanford Graduate School of Business appearance Sam Altman was recently quoted as saying “I no longer think we’re going to be able to just patch all the bugs” (source: Gizmodo, Oct 23, 2026, byline AJ Dellinger).
Question: In the age of AI being so good at finding security holes in software, would SPARK (say GOLD level?) be able to remove this threat?
Disclaimer: I know almost nothing about SPARK.
That’s quite literally a good use for this ai stuff, finding bugs. So, just proves he doesn’t know what he’s talking about.
Fair enough.
But the question was trying to ask if the strict use of SPARK would make it almost impossible to have any bugs to find (regardless of whether AI was used or not)?
My 2 cts.
First, AFAIK SPARK helps to prove the absence of errors in code. It doesn’t prove absence of errors in design. Second given the scale and the amount of code that needs to be changed to SPARK, it is totally unrealistic. Third, since SPARK code is a subset of Ada and Ada wasn’t designed to solve AI implementation I don’t think SPARK is the solution to Altman’s problems. Maybe Altman himself is part of the problem.
SPARK “thinking” and good design for new sw is a way forward. But I am afraid that the intellectual task to do this is to large and to complex for people who can generate code with the click of a button.
Personally I think SPARK can be part of the solution. Indeed you still need good design, and you need to check the contracts you write (or let the AI write) match what you want. If you have that, you can eliminate most bugs in the code that’s fully in SPARK. When generating SPARK with agents, the only types of crashes I ever had were stack overflows, as SPARK doesn’t check for those.
A programming language is just one of the tools to develop software. There are many other additional tools and methodologies that are used to make sure the software requirements, design, implementation and testing are done correctly.
If you look at a lot of open source (and commercial) software you will find badly documented spaghetti code. This is because many of the people who write that code engage is coding rather than software engineering.
You can write safe and secure software in any programming language, even assembly, provided you invest enough time and effort to review and verify it.
AI will not find all the overflows, ever. You can use SPARK to do that for code that is rewritten. Logic errors are less likely with higher levels of SPARK but still possible as already said the design could be wrong but a wrong cryptographic design for example is quite rare (ignoring e.g. json web tokens).
I didn’t say it could, i said it could be a good use for finding bugs, whatever it finds is still better than what the source was before.
But Sam and I kind of hate to agree with him (considering all the nonsense he has stated) apparently said “all the bugs” which should have been obvious.
I do believe the future is a parallel of Functional Core, Imperative Shell, “Verified Core, Unverified Shell.”
Verified core and leaf behavior, and then wrap it with less unverified code (less critical or things which are more difficult to verify).