431–440 of 448 posts
Earlier quoted context omitted.
So... a specification.
no ! a _design_ document. how this new thing will fit together with other things that are already existing in the system. what it’s interactions are going to look like, what are the assumptions, what are the limitations etc etc.
The funny part of “AI will make formal verification go mainstream” is that it skips over the one step the industry still refuses to do: decide what the software is supposed to do in the first place. We already have a ton of orgs that can’t keep a test suite green or write an honest invariant in a code comment, but somehow we’re going to get them to agree on a precise spec in TLA+/Dafny/Lean and treat it as a blocking…
There are some basic invariants like "this program should not crash on any input" or "this service should be able to handle requests that look like X up to N per second" — though I expect those will be the last to be amenable to formal verification, they are also very simple ones that (when they become possible) will be easy to write down.
In the world of Rust, this is actually the easiest to achieve level of formal proofs.
Simple lints can eliminate panics and potentially-panicking operations (forcing you/LLM to use variants with runtime error handling, e.g. `s[i]` can become `s.get(i).unwrap_or(MyError::RuhRoh)?`, or more purpose-specific handling; same thing for e.g. enforcing that arithmetic never underflows/overflows).
Kani symbolically evaluates simple Rust functions and ensures that the function does not panic on any possible value on it's input, and on top of that you can add invariants to be enforced (e.g. search for an item in an array always returns either None or a valid index, and the value at that index fulfills the search criteria).
(The real challenge with e.g. Kani is structuring a codebase such that it has those simple-enough subparts where formal methods are feasible.)
Earlier quoted context omitted.
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.
> 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 th…
Javascript:
let x = foo();
if (x.bar) { ... } // might blow up
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
I don't think formal verification really addresses most day-to-day programming problems: * A user interface is confusing, or the English around it is unclear * An API you rely on changes, is deprecated, etc. * Users use something in unexpected ways * Updates forced by vendors or open source projects cause things to break * The customer isn't clear what they want * Complex behavior between interconnected systems, out…
A change in the API of a dependency should be detected immediately and handled silently.
Reliance on unspecified behavior shouldn't happen in the first place; the client's verification would fail.
Detecting breakage caused by library changes should be where verification really shines; when you get the update, you try to re-run your verification, and if that fails, it tells you what the problem is.
As for interconnected systems, again, that's pretty much the whole point. Obviously, achieving this dream will require formalizing pretty much everything, which is well beyond our capabilities now. But eventually, with advances in AI, I think it will be possible. It will take something fundamentally better than today's LLMs, though.
Earlier quoted context omitted.
no ! a _design_ document. how this new thing will fit together with other things that are already existing in the system. what it’s interactions are going to look like, what are the assumptions, what are the limitations etc etc.
So... a specification.
Earlier quoted context omitted.
Peter Norvig once proposed to consider a really large grammar, with trillion rules, which could simulate some practically small applications of more complex systems. Many programs in practice don't need to be written in Turing-complete languages, and can be proven to terminate.
This sounds very interesting. Do you have a reference?
Earlier quoted context omitted.
Peter Norvig once proposed to consider a really large grammar, with trillion rules, which could simulate some practically small applications of more complex systems. Many programs in practice don't need to be written in Turing-complete languages, and can be proven to terminate.
Writing in a language that guarantees termination is not very interesting in itself, as every existing program could automatically be translated into a non-Turing-complete language where the program is proven to terminate, yet behaves exactly the same: the language is the same as the original, only loops/rectursion ends the program after, say, 2^64 iterations. This, in itself, does not make programs any easier to ana…
Earlier quoted context omitted.
Some type systems (e.g, Haskell) are closing in in becoming formal verification languages themselves.
Piggybacking off your comment, I just completed a detailed research paper where I compared Haskell to C# with an automated trading strategy. I have many years of OOP and automated trading experience, but struggled a bit at first implementing in Haskell syntax. I attempted to stay away from LLMs, but ended up using them here and there to get the syntax right. Haskell is actually a pretty fun language, although it does…
public int Fib(int n) => n switch
{
n,
_ => Fib(n - 1) + Fib(n - 2)
};Earlier quoted context omitted.
An analogy is asking someone who is colorblind how many colors are on a sheet of paper. What you are probing isn't reasoning, it's perception. If you can't see the input, you can't reason about the input.
> What you are probing isn't reasoning, it's perception. Its both. A colorblind person will admit their shortcomings and, if compelled to be helpful like an LLM is, will reason their way to finding a solution that works around their limitations. But as LLMs lack a way to reason, you get nonsense instead.
This assumes the colorblind person both believes it is true that they are colorblind, in a world where that can be verified, and possesses tools to overcome these limitations.
You have to be much more clever to 'see' an atom before the invention of a microscope, if the tool doesn't exist: most of the time you are SOL.
Earlier quoted context omitted.
> Most of the data I deal with are strings with their own validation and formatting rules that are complicated and at the same time usually need to be permissive this is exactly where a good type system helps: you have an unvalidated string and a validated string which you make incompatible at the type level, thus eliminating a whole class of possible mistakes. same with object ids, etc. don't need haskell for this,…
That's neat, I was about to ask which languages support that since the vast majority don't. I didn't know that you can do that in Typescript.
Even OOP : if you have a string class, you can have a String_Formated_For_API subtype.
Just extends String, and add some checking.
But now the type checker "knows" it can print() a String_Formated_For_API just fine but not call_API(string).