[burakemir]

I will quote (approximately) Simon Peyton Jones: "writing programs is not hard. Specifying what a program should do is hard."

Prove what? The author is well versed in the problem of specifications as the aliens-demand-gcc-correctness-or-else post. I also enjoyed the other post where they say "no one cares about correctness" and "people care about compliance".

It is safe to say, most people are not experts and will never become experts.

Being proficient in the business of coming up with suitable specification that can be implemented and getting assurance that an implementation meets the spec will most likely need all the kind of formal training for humans that the AI hype industry assures us is no longer necessary.

So it doesn't much help that LLMs are good at manipulating the tokens when used by experts, at least not in a big way. It can be hoped that they change cost-benefit balance in good ways, but the bigger problems of the industry will simply persist.

What would need to change for a more fundamental shift is getting a lot more people to understand the value of specifications. This is an education problem and paradoxically I could see AI helping a lot... if only there was enough interest in using AI to help humans become experts.

[baq]

This change is happening as we speak. My work repo is now sprouting with markdowns primarily intended for agentic consumption, but it’s all dense jargon communicating requirements and important design decisions in a way which is useful to me as a software engineer. The toil of writing these specs from low level code is much lower today, because LLMs also help with that immensely.

[ranyume]

In my workplace happens this, but in a bad way. There's a push to make use of AI as much as we can to "boost productivity", and the one thing people don't want to do is write documentation. So what ends up happening is that we end up with a bunch of AI documentation that other AIs consume but humans have a harder time following because of the volume of fluff and AI-isms. Shitty documentation still exists and can be worse than before...

[burakemir]

There is a place for informal, prose specs, and I can easily agree that more people are nowadays describing their programs in English.

The context here is formal specs though - adequately and precisely capturing the intended meaning (semantics) in a way that lends itself to formal verification.

Interactive theorem proving is interactive because proof search is intractable; a human articulates the property they want to prove and then performs the "search". Apart from the difficulties of getting to that proof, it can also happen that all goes through and you realize that the property is not exactly what you wanted.

[ares623]

I’m curious if your markdowns are discernible by other engineers? Or are they purely only discernible by you and an LLM?

[pron]

I think you're missing a more internecine debate within software correctness/formal methods circles than the more general one about "writing good/correct software". Deductive theorem proving was all the rage in the 1970s, to the point that prominent people (Tony Hoare, Dijkstra) believed that it's the only way to write correct software. Over the years, the focus has shifted to other methods [1], from model-checking to unsound methods such as concolic testing and even property-based testing and code reviews, which have proven more effective than the deductive proof proponents had envisioned (Tony Hoare admitted his mistake in the nineties).

The problem with deductive proofs is that it's all-or-nothing, i.e. either you prove the theorem or you don't, and it's much harder to turn a knob to trade off cost for confidence and vice-versa than with other methods. Consequently, theorem proving has not benefitted from automation as much as it's alternatives, and is now viewed as having a too low bang-for-the-buck. But if LLMs can help automate deductive theorem proving, maybe that particular approach, which has gradually become less popular within formal methods circles but still has its fans, could make a comeback.

Of coure, specification is equally important in all methods, but the particular method of theorem proving has been disadvantaged compared to other formal and semi-formal methods, and I think that's what the author wishes could change.

[1]: Deductive theorem proving may be more prominent on HN than other formal methods, but as with most things, HN is more representative of things that spark people's imagination than of things that work well. I'm not counting that as a strike against HN, but it's something to be aware of. HN is more Vogue/GQ than the Times, i.e. it's more news about what people wish they were doing than what they're actually doing.

[zozbot234]

> The problem with deductive proofs is that it's all-or-nothing, i.e. either you prove the theorem or you don't, and it's much harder to turn a knob to trade off cost for confidence and vice-versa than with other methods.

This is not really true though. Sound type checking is a kind of deductive proof, but it's practically usable because it establishes very simple properties and is generally "local", i.e. it follows the same structure as program syntax.

[brap]

>writing programs is not hard. Specifying what a program should do is hard.

But these two things are kinda the same thing. Writing a program is mostly just specifying what it should do in a very specific, unambiguous way. That’s why we have programming languages and don’t use English.

A PRD, a design doc and the code itself are kind of all the same thing, but with increasing levels of specification.

If you’ve ever played with formal specifications at some point you probably had the realization “wait a minute, I’m just writing another implementation of the program!” and in a way you are.

[bobro]

Spoken language descriptions of how to do something are incredibly underdetermined. Many people are likely familiar with the meme of following exact instructions on making a PB&J where a phrase like “put a knife in your hand and spread the peanut butter” can result in stabbing yourself and rubbing peanut butter on the wound. More than half of my job is helping other people know or otherwise determining what they really want a program to do in the first place.

[bambax]

This sounds true but isn't.

"The program should accept one parameter as a number, and output this number multiplied by two" is a spec.

  input a

  print a*2

is a program.

But: why do that? why multiply by two? what does two represent? what do the input and output mean in the real world? what part is likely to change in the near future? etc.

Wrting the program isn't harder than writing the spec. Analyzing the problem and coming up with solutions is the hard part.

(And yes, LLMs are getting better at this everyday, but I think they still have a very long way to go.)

[AfterHIA]

You read like Alan Kay's Quora and for that I salute you comrade.