61–70 of 72 posts
Earlier quoted context omitted.
Forall (n: Nat) Is perfectly reasonable. If conciseness was that important theorem provers would have syntax like APL.
Why is forall any less formal than ∀? Or Nat less formal than ℕ? Especially when these are symbols that most will have learned in high school?
I like there is us who like formal methods and guarantees of correctness for our code. And then there are the others who now generate approximately code with large language models that mostly runs. They are winning.
Often phrased as "worse is better."
Like, hypothetically, imagine you spent two whole weeks designing and implementing a new programming language, which was guaranteed to be installed on millions of computers overnight. Any language which took three weeks to finish, like wasting a week testing, would be DOA.
Like how the (brood parasite) cuckoo chick hatches early and then murders all the other chicks.
I like there is us who like formal methods and guarantees of correctness for our code. And then there are the others who now generate approximately code with large language models that mostly runs. They are winning.
I like there is us who like formal methods and guarantees of correctness for our code. And then there are the others who now generate approximately code with large language models that mostly runs. They are winning.
Imagine a programming system where you can specify little components using Hoare or Separation Logic, i.e. pre/postconditions. An engineer could spend his effort specifying little components, but code and proof generation can be handled by GPT. Actually, many tasks can be offloaded to a SAT/SMT solver. Lots of verification and synthesis efforts already do the last bit, offloading to SAT/SMT solver.
This would be a win-win. Formal methods would become cheaper to use, and software would become built using rigorous engineering.
Earlier quoted context omitted.
> I think I would just be easier to hit compile on that spec I have a hard time not being similarly skeptical about formal methods. They promise the ultimate holy grail of software development - release software with zero defects - but demand what appears to be years of study before you actually see results. On the one hand, there's lots of examples of techniques and tactics that promise amazing results if you "put i…
As someone who was working on this decades ago [1][2], here's a useful recap. - Back then, CPU power for the prover was a big problem. That's been fixed. We were too early in the days of a 1 MIPS VAX. - Prover theory is much better. We were using the Oppen-Nelson prover, the original SAT system. Now that's routine technology. - Loose languages are a problem. You have to nail down all "undefined behavior", and either…
Can a button be formally verified (or failed), if due to poor graphic design it may or may not look like a button?
Another "other extreme": create the source for a new database manager that formally matches the behavior of another database manager, that you only have object code for. :)
Sure, ChatGPT will successfully manage to find formal proofs that have been done before.
But synthesising proofs from scratch is NP-complete for the simplest proofs (or worse for more interesting cases), and LLMs are simply not clever enough to do it (except in cases where the proof has been seen before).
It could be possible to integrate an SMT solver with a LLM to make this work, but the core difficulty of the FM task will then be solved by the SMT solver.
To those wondering if there will be a successful "marriage" between popular incarnations of AI, like ChatGPT, and FM: no, at least not in the sense you would expect. Sure, ChatGPT will successfully manage to find formal proofs that have been done before. But synthesising proofs from scratch is NP-complete for the simplest proofs (or worse for more interesting cases), and LLMs are simply not clever enough to do it (ex…
Earlier quoted context omitted.
Do you have more to share? I use Alloy at work and research and would love to learn about how Apple uses FM.
Not at apple: The following is about 10 years out of date, would be interesting to know what's changed: 10 years ago formal had just started to be viable in run of the mill semiconductor verification (as opposed to throwing a bunch of specialist PhD grads at the problem); Jasper Gold was the first tool I heard of that worked well enough. pre-formal, the approach was to write a bunch of tests with input stimulators an…
https://blogs.synopsys.com/from-silicon-to-software/2021/02/...
Earlier quoted context omitted.
Not at apple: The following is about 10 years out of date, would be interesting to know what's changed: 10 years ago formal had just started to be viable in run of the mill semiconductor verification (as opposed to throwing a bunch of specialist PhD grads at the problem); Jasper Gold was the first tool I heard of that worked well enough. pre-formal, the approach was to write a bunch of tests with input stimulators an…
Synopsys has a production grade C-to-RTL sequential equivalence tool called HECTOR, with a focus on data path verification. https://blogs.synopsys.com/from-silicon-to-software/2021/02/...
https://www.cadence.com/ko_KR/home/tools/system-design-and-v...
Earlier quoted context omitted.
Synopsys has a production grade C-to-RTL sequential equivalence tool called HECTOR, with a focus on data path verification. https://blogs.synopsys.com/from-silicon-to-software/2021/02/...
So do Cadence with Jasper C2RTL. (Disclaimer; I work on Cadence Jasper Apps, formerly JasperGold) https://www.cadence.com/ko_KR/home/tools/system-design-and-v...