Hacker News new | past | comments | ask | show | jobs | submit
saidnooneever | on: LLMs are making formal software verification feasible at a much larger scale
the code is either single threaded or multi threaded. not partially...

so either you verify the whole thing or basically you didnt verify anything.

remember what verification is for. its great your query parser is functionally correct but verification is meant to prove something.

say you have a car. and its got safety requirements. those need to be verified. But now they say we've verified its safe only for the rear seat passengers. or, only the engine block is verified itll keep running safely.. it completely negates what is being done if its not done completely to the entire car.

and then ofc another driver just prangs into you anyway with their uncerified car, or suddenly the unverified road (OS) turns into a sinkhole and all ur verification still goes out the window..

there are limits already to verification if done properly and skipping the hard/important parts is really a big issue... u might aswell not do it.

(i do respect that there is a road to fully verified, u wont slap out those 9 million lines in one go. but saying you're winning halfway through the race.... nope)

solyin | parent
But the analogy falls short. If I'm running a foot race and stop to celebrate before the end, someone else is going finish the race and win. If we're going from single to multi-threaded code. Using whatever synchronization primitives exist on the system, each section that I'm able to complete means that part is able to run faster when used by a multi-threaded system. Maybe a better comparison is a triathlon then. If you finish the bicycling section. No one can take that from you, even if you don't finish the rest.