4 ms·

We are slowly getting there, SE is just a bit over 50 years old. For example, Dafny (by MSR) is relatively easy to use and scales nicely to build systems of 20-

by nextos 2y ago

We are slowly getting there, SE is just a bit over 50 years old. For example, Dafny (by MSR) is relatively easy to use and scales nicely to build systems of 20-30 KLOC with some formal guarantees. It's a nice imperative language where specifications are encoded as contracts, so quite familiar to developers. Costs are still relatively high obviously, and it won't scale to bigger systems. I think LLMs could help a lot to lower cost by providing some automation to turn specifications into code. DeepMind has already shown a proof of concept for mathematical theorems using Lean. I have a toy implementation for Isabelle oriented towards SE that works quite well.

abelcha 2y ago
Thats what the ai would say
deleted 2y ago
[deleted]
kragen 2y ago
that's exciting news! what does your toy implementation do?
- nextos 2y ago
  It translates natural language into Isabelle/HOL specifications, and then tries to fill these up to prove things. One can then use Isabelle code generation facilities to extract Scala, OCaml, etc. I think the trick is to have a programmer to guide the whole process, especially decomposition into different modules and abstractions.
  - kragen 2y ago
    what have you been able to get it to write so far?
    - kragen 2y ago
      (i hope this comment didn't sound skeptical or dismissive)
      - nextos 2y ago
        No worries! The comment was fine, I was simply gone so I couldn't reply. TBH, I haven't written anything impressive, just toy examples that are formally verified. I imagine making it practical for larger systems would require a lot more work.
        kragen 2y ago
        i'm curious to know what you mean by toy examples! are we talking about an assignment statement, an arithmetic expression, finding the maximum of a list, insertion sort, mergesort, a parser for a context-free language, a cooperative multithreading system?
        nextos 2y ago
        Some simple imperative data structures, including simple operations to add, remove, test membership, etc. with formal guarantees.
        kragen 2y ago
        that sounds awesome! what does the process of getting to one of those proofs look like? is there a lot of back and forth, or is it mostly autonomous?
        nextos 2y ago
        Mostly autonomous, with a bit of guidance, but this might be because the training set has examples that are similar enough, making interpolation easy.
        2y ago
  - versteegen 2y ago
    Nice. I agree that LLMs will be game-changing for easing the writing of specifications/contracts for verified code; it could become the standard. Interesting that you're using Isabelle/HOL for code generation. I'm working towards auto-formalization of maths using LLM translation to an intermediate language between English and the proof assistant (for which I'm leaning towards Isabelle/HOL) and then a toolbox of techniques (i.e. ATP) for the remaining translation. Formalization is too painful at the moment. It's nearly the same problem as yours. But I'm starting out on simpler problems. So I'm really interested in the "filling up" part, if you have anything to say about it.
amw-zero 2y ago
LLMs are really, really bad at proofs so far in my experience. Especially proofs in proof assistant since those are machine checked and unable to be faked.
nyrikki 2y ago
If you look at the proofs that Google solved, the fast one was similar to problems in Knuth, thus common in the corpus and the other two were reducible to exhaustive search, especially with lean4 feedback. Which is why they took more time than a human was given. There results were impressive, but not sufficient for SWE. If you note, it completely failed at the combinatorial problems. SW engineering is details, nuance, and tradeoffs. The specification problem that lead to an AI winter for expert systems still applies. If we could create good, exhaustive contracts, programming is easy. The failure of UML as a code generation tool is a good example. As LLMs are good at pattern finding, at least within the simplicity bias problem, I do think that they will have utility. But as an Enterprise Architect, form, complete specifications would completely remove the need for an LLM assistant as I could just write fitness functions and let the developers run with what they wanted. As we know LLMs are in context learners built of threshold circuits, they simply don't have the ability to consider tradeoffs and details. Funny enough this post has the smell of an author that wasn't aware of papers that came out in the previous couple years describing the specification problem.
- nextos 2y ago
  I agree, I am also not interested in a system that replaces humans. I am interested in a system that automates the boring parts and makes SWE simpler and closer to classical engineering disciplines while keeping humans in the loop. That is, an engineer would design and decompose the problem and the system would help to fill in the gaps in proofs. Sometimes this won't be possible, so the human engineer will need to redefine specifications or insert some intermediate lemmas.

by nextos 2y ago

abelcha 2y ago

Thats what the ai would say

deleted 2y ago

[deleted]

kragen 2y ago

that's exciting news! what does your toy implementation do?

nextos 2y ago
It translates natural language into Isabelle/HOL specifications, and then tries to fill these up to prove things. One can then use Isabelle code generation facilities to extract Scala, OCaml, etc. I think the trick is to have a programmer to guide the whole process, especially decomposition into different modules and abstractions.
- kragen 2y ago
  what have you been able to get it to write so far?
  - kragen 2y ago
    (i hope this comment didn't sound skeptical or dismissive)
    - nextos 2y ago
      No worries! The comment was fine, I was simply gone so I couldn't reply. TBH, I haven't written anything impressive, just toy examples that are formally verified. I imagine making it practical for larger systems would require a lot more work.
      - kragen 2y ago
        i'm curious to know what you mean by toy examples! are we talking about an assignment statement, an arithmetic expression, finding the maximum of a list, insertion sort, mergesort, a parser for a context-free language, a cooperative multithreading system?
        nextos 2y ago
        Some simple imperative data structures, including simple operations to add, remove, test membership, etc. with formal guarantees.
        kragen 2y ago
        that sounds awesome! what does the process of getting to one of those proofs look like? is there a lot of back and forth, or is it mostly autonomous?
        nextos 2y ago
        Mostly autonomous, with a bit of guidance, but this might be because the training set has examples that are similar enough, making interpolation easy.
        2y ago
- versteegen 2y ago
  Nice. I agree that LLMs will be game-changing for easing the writing of specifications/contracts for verified code; it could become the standard. Interesting that you're using Isabelle/HOL for code generation. I'm working towards auto-formalization of maths using LLM translation to an intermediate language between English and the proof assistant (for which I'm leaning towards Isabelle/HOL) and then a toolbox of techniques (i.e. ATP) for the remaining translation. Formalization is too painful at the moment. It's nearly the same problem as yours. But I'm starting out on simpler problems. So I'm really interested in the "filling up" part, if you have anything to say about it.

amw-zero 2y ago

LLMs are really, really bad at proofs so far in my experience. Especially proofs in proof assistant since those are machine checked and unable to be faked.

nyrikki 2y ago

If you look at the proofs that Google solved, the fast one was similar to problems in Knuth, thus common in the corpus and the other two were reducible to exhaustive search, especially with lean4 feedback. Which is why they took more time than a human was given. There results were impressive, but not sufficient for SWE. If you note, it completely failed at the combinatorial problems. SW engineering is details, nuance, and tradeoffs. The specification problem that lead to an AI winter for expert systems still applies. If we could create good, exhaustive contracts, programming is easy. The failure of UML as a code generation tool is a good example. As LLMs are good at pattern finding, at least within the simplicity bias problem, I do think that they will have utility. But as an Enterprise Architect, form, complete specifications would completely remove the need for an LLM assistant as I could just write fitness functions and let the developers run with what they wanted. As we know LLMs are in context learners built of threshold circuits, they simply don't have the ability to consider tradeoffs and details. Funny enough this post has the smell of an author that wasn't aware of papers that came out in the previous couple years describing the specification problem.

nextos 2y ago
I agree, I am also not interested in a system that replaces humans. I am interested in a system that automates the boring parts and makes SWE simpler and closer to classical engineering disciplines while keeping humans in the loop. That is, an engineer would design and decompose the problem and the system would help to fill in the gaps in proofs. Sometimes this won't be possible, so the human engineer will need to redefine specifications or insert some intermediate lemmas.