6 ms·

This is obviously a snapshot in time (title includes 1988). I can’t attest to the State of Computer Science Education in the late 1980s. He laments the term sof

This is obviously a snapshot in time (title includes 1988). I can’t attest to the State of Computer Science Education in the late 1980s. He laments the term software engineering because software engineering does not fit the traditional, more mechanical engineering terms. The more mathematical proof style that he is advocating for is used sometimes in aerospace (in particular Airworthiness) and medical. Some might say that his proposed methods only apply to software requiring that level of rigor. It is also really expensive.

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
- 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.
devjab 2y ago
It depends on which parts of software engineering you work in. If you work anywhere where performance matters people tend to know how computers work. If you work in 90% of software engineering you’re likely actively writing code which is terrible from an engineering perspective. Look at how popular things like SOLID and Clean Code in general are. When they are a direct path to horrible performance as you enter the area of L1 cache misses and vtavles on even an extremely simple function. It’s so weird to switch between working close to the hardware and working high above. Especially because Clean Code doesn’t actually seem easier to read or indeed maintain. As an external examiner for CS students I can’t say I’m surprised. They aren’t taught science anymore, they’re taught practices and patterns, and since nobody knows how a computer actually works or how to write performant code it’s easy for various grifters to sell them nonsense. I mean, how well would Clean Code, SOLID and to some degree Agile really sell if people knew the key people behind these things haven’t worked in software engineering since 20 years before Python was even invented? Probably not so well.
- jimbob45 2y ago
  When they are a direct path to horrible performance as you enter the area of L1 cache misses and vtavles on even an extremely simple function. It’s so weird to switch between working close to the hardware and working high above. Especially because Clean Code doesn’t actually seem easier to read or indeed maintain. If it's not on the critical path, what difference does it make? Code outside the critical path should be optimizing for something and maintainability is as good as anything.
  - funcDropShadow 2y ago
    GP said > Especially because Clean Code doesn’t actually seem easier to read or indeed maintain If that is true, then there is indeed no point in applying Clean Code. But I disagree with GP that Clean Code leads automatically to bad performing code. That depends on your language and execution environment. A JVM is very good at effectively removing vtable indirection if they are not needed at runtime.
    - 2y ago
lazide 2y ago
Very few domains where software is used now make sense for that level of rigor, in practice. At least with current levels of available staffing. The vast majority of software is being developed more akin to ‘residential construction’ type levels of investment rather than even ‘commercial construction’ or ‘major engineering projects’. Which makes sense. Rules of thumb work well enough most of the time, and when it’s actually important (say a structure member, ahem, crypto library) then it makes sense to get it looked at more carefully by someone who more deeply understands what is going on. Though I don’t think we have a solid idea of what those areas are yet, let alone have codified them. So YOLO.
- jaybrendansmith 2y ago
  Great post. Yes when your GC or carpenter needs to remove a wall, they bring in a real structural engineer. These roles exist for software engineering also. Only thing we are missing is a real licensing and governance body.
  - lazide 2y ago
    Well, and some sort of stable target to aim at regarding ‘important’. There is pretty solid consensus in construction that things like foundation design, structural walls/supports, projects over a given size, etc. need engineering sign off. There is no such consensus I can see right now on the software side, and software projects are also a lot more complex than a typical construction project in ways that are hard to quantify. How would you even define a licensing test that wouldn’t be obsolete in a year or two even?

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

devjab 2y ago

It depends on which parts of software engineering you work in. If you work anywhere where performance matters people tend to know how computers work. If you work in 90% of software engineering you’re likely actively writing code which is terrible from an engineering perspective. Look at how popular things like SOLID and Clean Code in general are. When they are a direct path to horrible performance as you enter the area of L1 cache misses and vtavles on even an extremely simple function. It’s so weird to switch between working close to the hardware and working high above. Especially because Clean Code doesn’t actually seem easier to read or indeed maintain. As an external examiner for CS students I can’t say I’m surprised. They aren’t taught science anymore, they’re taught practices and patterns, and since nobody knows how a computer actually works or how to write performant code it’s easy for various grifters to sell them nonsense. I mean, how well would Clean Code, SOLID and to some degree Agile really sell if people knew the key people behind these things haven’t worked in software engineering since 20 years before Python was even invented? Probably not so well.

jimbob45 2y ago
When they are a direct path to horrible performance as you enter the area of L1 cache misses and vtavles on even an extremely simple function. It’s so weird to switch between working close to the hardware and working high above. Especially because Clean Code doesn’t actually seem easier to read or indeed maintain. If it's not on the critical path, what difference does it make? Code outside the critical path should be optimizing for something and maintainability is as good as anything.
- funcDropShadow 2y ago
  GP said > Especially because Clean Code doesn’t actually seem easier to read or indeed maintain If that is true, then there is indeed no point in applying Clean Code. But I disagree with GP that Clean Code leads automatically to bad performing code. That depends on your language and execution environment. A JVM is very good at effectively removing vtable indirection if they are not needed at runtime.
  - 2y ago

lazide 2y ago

Very few domains where software is used now make sense for that level of rigor, in practice. At least with current levels of available staffing. The vast majority of software is being developed more akin to ‘residential construction’ type levels of investment rather than even ‘commercial construction’ or ‘major engineering projects’. Which makes sense. Rules of thumb work well enough most of the time, and when it’s actually important (say a structure member, ahem, crypto library) then it makes sense to get it looked at more carefully by someone who more deeply understands what is going on. Though I don’t think we have a solid idea of what those areas are yet, let alone have codified them. So YOLO.

jaybrendansmith 2y ago
Great post. Yes when your GC or carpenter needs to remove a wall, they bring in a real structural engineer. These roles exist for software engineering also. Only thing we are missing is a real licensing and governance body.
- lazide 2y ago
  Well, and some sort of stable target to aim at regarding ‘important’. There is pretty solid consensus in construction that things like foundation design, structural walls/supports, projects over a given size, etc. need engineering sign off. There is no such consensus I can see right now on the software side, and software projects are also a lot more complex than a typical construction project in ways that are hard to quantify. How would you even define a licensing test that wouldn’t be obsolete in a year or two even?