News for hackers. Stuff that matters.
Re:Prediction: AI will make formal verification go mainstream by elbear on Wednesday December 17, 2025 @03:12AM (#46299434)
> No one claims that good type systems prevent buggy software.

That's exactly what languages with advanced type systems claim. To be more precise, they claim to eliminate entire classes of bugs. So they reduce bugs, they don't eliminate them completely.

Re:Prediction: AI will make formal verification go mainstream by bonesss on Wednesday December 17, 2025 @03:37AM (#46299580)
No nulls, no nullability bombs.

Forcing devs to pre-fix/avoid bugs before the compiler will allow the app means the programs are more correct as a group.

Wrong, incomplete, insufficient, unhelpful, unimpressive, and dumb are all still very possible. But more correct than likely in looser systems.

Re:Prediction: AI will make formal verification go mainstream by fc417fc802 on Wednesday December 17, 2025 @09:42PM (#46308376)
> No nulls, no nullability bombs.

I hate this meme. Null indicates something. If you disallow null that same state gets encoded in some other way. And if you don't properly check for that state you get the exact same class of bug. The desirable type system feature here is the ability to statically verify that such a check has occurred every time a variable is accessed.

Another example is bounds checking. Languages that stash the array length somewhere and verify against it on access eliminate yet another class of bug without introducing any programmer overhead (although there generally is some runtime overhead).

Re:Prediction: AI will make formal verification go mainstream by yencabulator on Thursday December 18, 2025 @01:30PM (#46316597)
The whole point of "no nullability bombs" is to make it obvious in the type system when the value might be not present, and force that to be handled.

Javascript:

  let x = foo();
  if (x.bar) { ... } // might blow up
Typescript:

  let x = foo(); // type of x is Foo | undefined
  if (x === undefined) { ...; return; } // I am forced to handle this
  if (x.bar) { ... } // this is now safe, as Typescript knows x can only be a Foo now
(Of course, languages like Rust do that cleaner, since they don't have to be backwards-compatible with old Javascript. But I'm using Typescript in hopes of a larger audience.)
Re:Prediction: AI will make formal verification go mainstream by kazinator on Wednesday December 17, 2025 @04:25AM (#46299876)
If you eliminate the odd integers from consideration, you've eliminated an entire class of integers. yet, the set of remaining integers is of the same size as the original.
Re:Prediction: AI will make formal verification go mainstream by moi2388 on Wednesday December 17, 2025 @08:02AM (#46301489)
No, because integers in computing are generally finite.
Re:Prediction: AI will make formal verification go mainstream by petesergeant on Wednesday December 17, 2025 @04:55AM (#46300049)
Peak HN gnomism. While the set of possible errors may be infinite, their distribution is not uniform.
Re:Prediction: AI will make formal verification go mainstream by tmtvl on Wednesday December 17, 2025 @01:06PM (#46303156)
There cannot be infinite bugs in a limited program.
Re:Prediction: AI will make formal verification go mainstream by Hercuros on Wednesday December 17, 2025 @04:04PM (#46305480)
How do you count how many bugs a program has? If I replace the Clang code base by a program that always outputs a binary that prints hello world, how many bugs is that? Or if I replace it with a program that exits immediately?

Maybe another example is compiler optimisations: if we say that an optimising compiler is correct if it outputs the most efficient (in number of executed CPU instructions) output program for the every input program, then every optimising compiler is buggy. You can always make it less buggy by making more of the outputs correct, but you can never satisfy the specification on ALL inputs because of undecidability.

Re:Prediction: AI will make formal verification go mainstream by kazinator on Wednesday December 17, 2025 @02:36PM (#46304423)
Programs are not limited; the number of Turing machines is countably infinite.

When you say things like "eliminate a class of bugs", that is played out in the abstraction: an infinite subset of that infinity of machines is eliminated, leaving an infinity.

How you then sample from that infinity in order to have something which fits on your actual machine is a separate question.

Re:Prediction: AI will make formal verification go mainstream by gls2ro on Wednesday December 17, 2025 @01:39PM (#46303613)
Because the number of state where a program can be is so huge (when you consider everything that can influence how a program runs and the context where and when it runs) it is for the current computation power practically infinite but yes it is theoretically finite and can even be calculated.