Hacker News Reader

Comment by firesteelrain | Hacker News Reader

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.

View on HN

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.

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.

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.

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.

Thats what the ai would say

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

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.

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.

what have you been able to get it to write so far?

(i hope this comment didn't sound skeptical or dismissive)

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.

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?

Some simple imperative data structures, including simple operations to add, remove, test membership, etc. with formal guarantees.

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?

Mostly autonomous, with a bit of guidance, but this might be because the training set has examples that are similar enough, making interpolation easy.

fantastic! i hope you decide to share more details; i'd love to hear them

Thanks. It's a toy at the minute, there is nothing super impressive.

Taking this forward would require a lot more work and funding to pay for computation to fine-tune models further.

It's an interesting topic, perhaps good for a startup or a research lab in case one finds a decent monetization stream.

pretty sure you'll be able to monetize writing correct software at scale with an llm

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.

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.

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?

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.

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.

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.

I don't think a compiler could ever reliably transpose an array-of-structs representation to a struct-of-arrays one.

There's also other issues with this paradigm, like creating objects out of the arguments to a function. That not only makes your code less maintainable (what if you need a subset of the variables), but now you'll have to drag all that data to each function you create.

Clean code is, IMO, worthless, data- and domain-driven design practices accomplish the goals of clean code better than it the paradigm itself does, and also improve other considerations like correctness and performance.

>I don't think a compiler could ever reliably transpose an array-of-structs representation to a struct-of-arrays one.

An interesting question, but a SoA isn't necessarily better than an AoS: it depends on the access pattern, so the question is whether this optimisation could be added as a part of PGO..

I'd also argue that even if vtable indirection can't be removed, it's unlikely to be a notable part of your performance profile, at least in the general case. Profile! You might instead see the hasher for your hash table has a much bigger.

The critical path can often be very wide and long and is not some small for loop deep down. Not all software is a video codec. Maintainability also does not necessarily exclude performance, smaller code can be easier to grasp and fit better into caches.

I’d argue that splitting what is essentially a four line check or default into something like three different functions makes it a lot harder to grasp.

I think my issue with clean code is primarily that it doesn’t actually make code more maintainable. As another poster mentioned, data or domain driven design does the same thing better.

Reply on news.ycombinator.com