Hacker News new | past | comments | ask | show | jobs | submit
imtringued | on: LLMs are making formal software verification feasible at a much larger scale
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.

deterministic | parent | next
Not my experience at all. I have added multi-threading to very large C++ applications safely. One of them has been used in production for 5+ years without a single bug. The trick is to do it very carefully and use automatic tools (Valgrind etc.) to verify the code.
naasking | parent | next
> or the retrofit is going to be painful and probably will never happen.

They're using LLMs. The economics of this sort of retrofit has changed considerably with LLMs.

octoberfranklin | 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.