Hacker News new | past | comments | ask | show | jobs | submit
malisper | on: LLMs are making formal software verification feasible at a much larger scale
Proving the code works single threaded is a stepping stone to eventually proving the code works under concurrency. It may be surprising, but very little of the Postgres code deals with concurrency. For the most part they've isolated the parts that deal with concurrency to a small number of subsystems. At least by volume of code, the vast majority of it is single threaded
saidnooneever | parent | next
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)

loading story #50206578
imtringued | parent
This type of logic only works in Rust or Haskell but basically no other programming language.

If you use a language like Java, you have to start with a multi threading aware design concept first or the retrofit is going to be painful and probably will never happen.

Multi threading in classical programming languages with mutable aliasing by default requires global program analysis to check if it is safe or not. Rust restricts the programs to what can be reasoned locally.

loading story #50217357
loading story #50207840
octoberfranklin | root | parent
It only works in Rust if you have code that is parallel-without-concurrency.

Databases and operating systems are inherently concurrent. They deal with concurrency sources outside the process running the Rust code. Because of this, they don't get the magical shared-xor-mutable => deterministic-concurrency benefit that Rust is famous for.

And, frankly, if you tried to make SQL/ACID shared-xor-mutable you'd completely cripple it. Databases are inherently concurrent.