Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Dijkstra On the foolishness of "natural language programming"

cs.utexas.edu

Post reply on HN
Print view View original

231–240 of 281 posts

Re: Dijkstra On the foolishness of "natural language programming"

#231

Post by stouset »

fourside wrote: post #132
eightysixfour wrote: post #127

Earlier quoted context omitted.

Language can carry tremendous amounts of context. For example: > I want a modern navigation app for driving which lets me select intersections that I never want to be routed through. That sentence is low complexity but encodes a massive amount of information. You are probably thinking of a million implementation details that you need to get from that sentence to an actual working app but the opportunity is there, the…

You call it context or information but I call it assumptions. There are a ton assumptions in that sentence that an LLM will need to make in order to take that and turn it into a v1. I’m not sure what resulting app you’d get but if you did get a useful starting point, I’d wager the fact that you chose a variation of an existing type of app helped a lot. That is useful, but I’m not sure this is universally useful.

Dingdingding

Since none of those assumptions are specified, you have no idea which of them will inexplicably change during a bugfix. You wanted that in cornflower blue instead, but now none of your settings are persisted in the backend. So you tell it to persist the backend, but now the UI is completely different. So you specify the UI more precisely, and now the backend data format is incompatible.

By the time you specify all the bits you care about, maybe you start to think about a more concise way to specify all these requirements…

Re: Dijkstra On the foolishness of "natural language programming"

#232

Post by codebje »

School-Cotton wrote: post #220
whatevertrevor wrote: post #219

Earlier quoted context omitted.

Textbooks aren't just communicating theorems and proofs (which are often just written in formal symbolic language), but also the language required to teach these concepts, why these are important, how these could be used and sometimes even the story behind the discovery of fields. So this is far from an accurate comparison.

Theorems and proofs are almost never written in formal symbolic language.

My experience in reading computer science papers is almost exactly the opposite of yours: theorems are almost always written in formal symbolic language. Proofs vary more, from brief prose sketching a simple proof to critical components of proofs given symbolically with prose tying it together.

(Uncommonly, some papers - mostly those related to type theory - go so far as to reference hundreds of lines of machine verified symbolic proofs.)

Re: Dijkstra On the foolishness of "natural language programming"

#233

Post by School-Cotton »

codebje wrote: post #232
School-Cotton wrote: post #220

Earlier quoted context omitted.

Theorems and proofs are almost never written in formal symbolic language.

My experience in reading computer science papers is almost exactly the opposite of yours: theorems are almost always written in formal symbolic language. Proofs vary more, from brief prose sketching a simple proof to critical components of proofs given symbolically with prose tying it together. (Uncommonly, some papers - mostly those related to type theory - go so far as to reference hundreds of lines of machine veri…

Can you give an example of the type of theorem or proof you're talking about?

Re: Dijkstra On the foolishness of "natural language programming"

#234

Post by smcin »

shit_game wrote: post #172
drpixie wrote: post #45

Earlier quoted context omitted.

> Do you find the resulting natural language description is easier to reason about? An example from an different field - aviation weather forecasts and notices are published in a strongly abbreviated and codified form. For example, the weather at Sydney Australia now is: METAR YSSY 031000Z 08005KT CAVOK 22/13 Q1012 RMK RF00.0/000.0 It's almost universal that new pilots ask "why isn't this in words?". And, indeed, mos…

> Same for maths and coding - once you reach a certain level of expertise, the complexity and redundancy of natural language is a greater cost than benefit. This seems to apply to all fields of expertise. And as well as these points, ambiguity . A formal specification of communication can avoid ambiguity by being absolute and precise regardless of who is speaking and who is interpreting. Natural languages are riddled…

Sure, but much ambiguity is trivially handled with a minimum amount of context. "Tomorrow I'm flying from Austin to Atlanta and I need to return the rental". (Is the rental (presumably car) to be returned to Austin or Atlanta? Almost always Austin, absent some unusual arrangement. And presumably to the Austin airport rental depot, unless context says it was another location. And presumably before the flight, with enough timeframe to transfer and checkin.)

(You meant inherent ambiguity in actual words, though.)

Re: Dijkstra On the foolishness of "natural language programming"

#235

Post by me-vs-cat »

fnord77 wrote: post #223
drpixie wrote: post #45

Earlier quoted context omitted.

> Do you find the resulting natural language description is easier to reason about? An example from an different field - aviation weather forecasts and notices are published in a strongly abbreviated and codified form. For example, the weather at Sydney Australia now is: METAR YSSY 031000Z 08005KT CAVOK 22/13 Q1012 RMK RF00.0/000.0 It's almost universal that new pilots ask "why isn't this in words?". And, indeed, mos…

I wonder why the legal profession sticks to natural language

Backwards compatibility works differently there, and legalese has not exactly evolved naturally.

Re: Dijkstra On the foolishness of "natural language programming"

#236

Post by centra_minded »

Modern programming already is very, very far from strict obedience and formal symbolism. Most programmers these days (myself included!) are using libraries, frameworks, and other features that mean what they are doing in practice is wielding sky-high abstractions, gluing things together they do not (and can not) fully understand the inner workings of.

If I create a website with Node.js, I’m not manually managing memory, parsing HTTP requests byte-by-byte, or even attempting to fully grasp the event loop’s nuances. I’m orchestrating layers of code written by others, trusting that these black boxes will behave as advertised according to my best, but deeply incomplete, understanding of them.

I'm not sure what this means for LLMs programming, but I already feel separated from the case Dijkstra lays out.

Re: Dijkstra On the foolishness of "natural language programming"

#237

Post by 0xbadcafebee »

I read this when I was younger, but I only now get it, and realize how true it all is.

13) Humans writing code is an inherently flawed concept. Doesn't matter what form the code takes. Machine code, assembly language, C, Perl, or a ChatGPT prompt. It's all flawed in the same way. We have not yet invented a technology or mechanism which avoids it. And high level abstraction doesn't really help. It hides problems only to create new ones, and other problems simply never go away.

21) Loosely coupled interfaces made our lives easier because it forced us to compartmentalize our efforts into something manageable. But it's hard to prove that this is a better outcome overall, as it forces us to solve problems in ways that still lead to worse outcomes than if we had used a simpler [formal] logic.

34) We will probably end up pushing our technical abilities to the limit in order to design a superior system, only to find out in the end that simpler formal logic is what we needed all along.

55) We're becoming stupider and worse at using the tools we already have. We're already shit at using language just for communicating with each other. Assuming we could make better programs with it is nonsensical.

For a long time now I've been upset at computer science's lack of innovation in the methods we use to solve problems. Programming is stupidly flawed. I've never been good at math, so I never really thought about it before, but math is really the answer to what I wish programming was: a formal system for solving a problem, and a formal system for proving that the solution is correct. That's what we're missing from software. That's where we should be headed.

Re: Dijkstra On the foolishness of "natural language programming"

#238

Post by codebje »

School-Cotton wrote: post #233
codebje wrote: post #232

Earlier quoted context omitted.

My experience in reading computer science papers is almost exactly the opposite of yours: theorems are almost always written in formal symbolic language. Proofs vary more, from brief prose sketching a simple proof to critical components of proofs given symbolically with prose tying it together. (Uncommonly, some papers - mostly those related to type theory - go so far as to reference hundreds of lines of machine veri…

Can you give an example of the type of theorem or proof you're talking about?

Here's one paper covering the derivation of a typed functional LALR(1) parser in which derivations are given explicitly in symbolic language, while proofs are just prose claims that an inductive proof is similar to the derivation:

    https://scholar.google.com/scholar?&q=Hinze%2C%20R.%2C%20Paterson%2C%20R.%3A%20Derivation%20of%20a%20typed%20functional%20LR%20parser%20%282003%29
Here's one for the semantics of the Cedille functional language core in which proofs are given as key components in symbolic language with prose to to tie them together; all theorems, lemmas, etc are given symbolically.

    https://arxiv.org/abs/1806.04709
And here's one introducing dependent intersection types (as used in Cedille) which references formal machine-checked proofs and only provides a sketch of the proof result in prose:

   https://doi.org/10.1109/LICS.2003.1210048
(For the latter, actually finding the machine checked proof might be tricky: I didn't see it overtly cited and I didn't go looking).

Re: Dijkstra On the foolishness of "natural language programming"

#239

Post by tired-turtle »

centra_minded wrote: post #236

Modern programming already is very, very far from strict obedience and formal symbolism. Most programmers these days (myself included!) are using libraries, frameworks, and other features that mean what they are doing in practice is wielding sky-high abstractions, gluing things together they do not (and can not) fully understand the inner workings of. If I create a website with Node.js, I’m not manually managing memo…

> Modern programming already is very, very far from strict obedience and formal symbolism

Difficult to sort this out with what follows.

Consider group theory. A group G is a set S with an operator * that supports an identity, closure, and an inverse. With that abstraction comes a hefty amount of power. In some sense, a group is akin to a trait on some type, much like how a class in Java can implement or extend Collection. (Consider how a ring ‘extends’ a group.)

I’d posit frameworks and libraries are no different in terms of formal symbolism from the math structure laid out above. Maybe the interfaces are fuzzy and the documentation is shoddy, but there’s still a contract we use to reason about the tool at hand.

> I’m not manually managing memory, parsing HTTP requests byte-by-byte

If I don’t reprove Peano’s work, then I’m not really doing math?

Re: Dijkstra On the foolishness of "natural language programming"

#240

Post by RainyDayTmrw »

fnord77 wrote: post #223
drpixie wrote: post #45

Earlier quoted context omitted.

> Do you find the resulting natural language description is easier to reason about? An example from an different field - aviation weather forecasts and notices are published in a strongly abbreviated and codified form. For example, the weather at Sydney Australia now is: METAR YSSY 031000Z 08005KT CAVOK 22/13 Q1012 RMK RF00.0/000.0 It's almost universal that new pilots ask "why isn't this in words?". And, indeed, mos…

I wonder why the legal profession sticks to natural language

They don't, though. Plenty of words in law mean something precise but utterly detached from the vernacular meaning. Law language is effectively a separate, more precise language, that happens to share some parts with the parent language.
Post reply on HN