58 ms·
I answered this to myself - stop worrying about LLMs. It's pretty simple: due to Curry-Howard isomorphism, programming languages are just notations for some typ
by js8 16d ago
I answered this to myself - stop worrying about LLMs. It's pretty simple: due to Curry-Howard isomorphism, programming languages are just notations for some type of formal logic.
Now ask yourself a question, what language do you want to maintain the programs in? Do you think natural language is going to be easier and more maintainable than formal logic?
The answer is no. So you need programmers, people who can read the formal description and adapt it to new requirements.
LLMs are amazing technology, but the truth is - natural language just kinda sucks. Therefore, you don't really need them (see also https://en.wikipedia.org/wiki/AI_effect https://en.wikipedia.org/wiki/AI_effect ).
I think people love LLMs for the same reasons they love magicians. But just like the magician employs a hidden trick, LLM just runs some algorithm you don't see or understand.
So worrying about LLMs taking programming job is kinda like worrying that a magician will take a warehouse worker job, because they can levitate stuff. Meanwhile, we already have automated programmer - it's called a compiler.
- jappgar 16d agoNo offense, but "natural language sucks" is the refuge of the illiterate logician. Complex language is clearly superior in nature. We're now finding out that that is true in computation as well.
- js8 16d agoI am not sure what your counterargument is. But in mathematics and computation, people have tried for at least 150 years to move away from natural language, and figure out stable foundations that can be externalized. I think there is a good reason for that - you save time correcting errors due to different interpretation.
- mrits 16d agoExtraneous and ambiguous is superior? Or are you talking about hypothetical new spoken languages?
- jappgar 15d agoYes. Ambiguity is a feature, not a bug.
- osmukka 15d agoIsn't code supposed to be exact? Pretty much the opposite of ambiguous.
- mrits 15d agoI don't think it's a feature or a bug. It is an indicator of an extremely poor spec though.
- datsci_est_2015 15d agoYes all of my the customers of my accounting software love the ambiguity of how it will react to them processing entries. You’re not saying anything with substance, but I guess that’s not surprising given your stance on LLMs.
- johnnyanmac 16d agoWe are in fact finding out precisely why natural language sucks in real time, as we have all kinds of catastrophic errors with people who think this is finally the time for complex language to prevail over pesky nerd language. The only difference is that more people seem to prescribe to the "you're holding it wrong" handwave when said catastrophes are pointed out.
- jappgar 15d agoPlenty of catastrophes are available under pure logic as well. The only catastrophes they prevent are accidental ones. Natural language can build civilization around "do unto others as you would have done unto you". Logic cannot encode morality, precisely because it is unambiguous.
- lioeters 15d ago> Logic cannot encode morality That doesn't even make sense, but you're arguing against logic so perhaps it's internally consistent.
- johnnyanmac 15d agoYou are right, and that is precisely the issue. When complex logic fails, we don't usually blame the machine. When natural language fails, we as of late seem to be trying to anthropomorphize a machine that cannot be held accountable. As if understanding natural language suddenly means it understands morals.
- ux266478 15d agoI can appreciate your original point, but this degenerated into naivete. The is-ought problem exists in (and was formulated for) natural language, and ambiguous formal languages are childsplay. There are further problems (ignorance of the consequences of reality being finite, misunderstanding the operative layers of interpretation) but these two alone are disastrous by themselves. Don't mix up convention with implicit substance. There's a very basic philosophical lesson you're missing, and I'll let you in on the secret: The labels aren't actually descriptions of any property. The distinction is indoor baseball. Notations, syntax, semantics. What you want is signal, and you can transmit that any way you want. Writing and drawing were once the same thing. Still are.
- juvvel 15d agoWell, almost all scientific domains have developed a form of structured and formal language, because natural language is too ambiguous. There's "code" everywhere, not just in programming.
- lioeters 15d agoNo offense but you're just making statements without backing it up with anything. "Clearly superior", "finding out that is true".. How are you going to prove what you said? Natural language is not enough for that purpose. You need formal logic, quantifications, specifications, the foundation of programming. Superior to what, and according to what metrics? What truth in computation are you talking about, and how can we know and confirm it? Not with natural language, but with numbers, mathematics, the building blocks of logic.
- jappgar 15d agoSuperior just means "above" or "on top of". Natural animals don't communicate in logical terms, even if their dna is a logical sequence.
- deleted 15d ago[deleted]
- deleted 15d ago[deleted]
- 0x445442 16d agoI agree with this but what I've been trying to answer the last few months is if there was an optimal language for the spec. As with you, I don't think it's English Markdown, but I don't think it's Java either. I also don't think it's Gherkin, Lisp perhaps? I'm still searching.
- js8 16d agoWell.. I think this is a big open problem in philosophy. On one hand, you have things like Lean (calculus of inductive constructions), these are relatively simple formal logics (just in more practical notation) that let you define any conceivable type, which is akin to specification. On the other hand, there is a rich set of modal and fuzzy logics that can help with aspects of reasoning in natural language. I think these can be defined in the former, but nobody has really made a good agreement as to how. So the main difficulty is for any such language to gain traction, people who speak it. Instead, we trained LLMs and they came up with something (evolved to reason). I think the future philosophical research will need to answer what exactly do LLMs bring to the table in terms of formalization of natural language.
- layer8 15d agoIn any case, it should be a formal language, and we haven’t finished exploring that space. I don’t expect that we will have anytime soon.
- jeremyjh 16d agoLLMs do not execute natural language. Natural language describes a problem or request, and LLMs generate and test formal logic they predict will satisfy the request.
- js8 16d agoI disagree with each sentence for a different reason. LLMs interpret (so, "execute" in a way) natural language in the sense they have internal logic that assigns to the sequence of tokens in context a next token. If we delineate the input and output into a series of logical statements, we can think of it as a program that builds a logical statement from a list of input statements. So it encodes derivation in some logical system. However, the internal logical system is informal in the sense that the above rules are not guaranteed to be sound on the fragment of classical logic encoded in the natural language. It is a close approximation, though, so it often works. To add, half of my problem with natural language would be resolved by agreeing on exact definitions, which is kinda what LLMs do internally. However, they don't surface this formalization very well(even with open weights it's difficult), which makes it pretty unusable.
- jeremyjh 15d ago> LLMs interpret (so, "execute" in a way) natural language You could say the same thing about human programmers, but I've never heard anyone say they think that programmers "execute" Jira tickets. > they have internal logic that assigns to the sequence of tokens in context a next token. I don't think this means what you think it means, because it has almost no information content relevant to what we're discussing. The probabilities that are most relevant at the level we're discussing are satisfying a reward function from post-training, which approximates to: "What is the likelihood the solution the agent is pursuing will be marked correct by the automated grader based on the full prompt and other context provided?" It still has to predict the next token but that isn't based on a likelihood of that token appearing in a corpus of internet text consumed in pretraining. That was eons ago. Every predicted token is shaped by the probabilities of the predicted solution, which must already be very specific and shaped completely by the request and associated context that is built during investigation of the same.
- henitchobisa 16d ago[dead]
- ds_opseeker 16d agore: natural language sucks. prof.dr.Edsger W.Dijkstra's views: https://www.cs.utexas.edu/~EWD/transcriptions/EWD06xx/EWD667.html https://www.cs.utexas.edu/~EWD/transcriptions/EWD06xx/EWD667... I humbly add my own. Natural language is valuable for the things it doesn't say. The ambiguity is core to the functionality. Which can be very helpful when navigating social complexities. And then written language is also valuable for the things IT doesn't say. Under the theory that 90% of communication is non-verbal, then writing lets you say things without having to communicate that other 90%. Which can be very helpful when negotiating something, for example.
- js8 15d agoI would agree with EDW, and I have argued here in a similar way. I am not against use of NL in negotiation or poetry. If you find ambiguity useful there, be my guest. But engineering specifications, mathematics, as well as other sciences or even philosophy would IMHO benefit from more rigor. I also strongly disagree with the notion that logical or programming languages cannot express ambiguity. (It actually took me many years to understand.) I used to think you need something like fuzzy logic or probability, but that's unsatisfactory in some ways. Eventually, I settled for a really simple understanding of the problem. Take lambda calculus for instance. I define the term to be ambiguous iff it has a normal form. So it is ambiguous if it expects additional argument, which resolves (part of or all) the ambiguity. Terms with no normal form are completely unambiguous, their "output" is completely given. In classical logic, this corresponds to formulas that are conditioned on additional assumption. Again, the extra assumption can resolve the ambiguity. So it is kind of my conviction (although we could show that by translating an LLM as a program into LC) that all the words in natural language can be formalized as sufficiently complicated lambda terms, that all have normal forms and react to each other in a way that resolves some ambiguity without ever resolving all of it.
- 1718627440 15d agoI wanted to bookmark this essay, only to find out I already had! Thanks.
- sanderjd 15d agoI totally agree with the skepticism that we'll ever get to a point where natural language becomes the "formalism" and stop needing people who understand the actual formalism underneath. And I agree that you don't need LLM based tools. But things that you don't need can still be (and often are) incredibly useful. Nobody needs an IDE, nobody needs vim or emacs or bash or even compilers or assemblers. But we have all those tools and they are useful. That is, their utility is net positive. Using LLMs to generate code currently also has (wildly) net positive utility. Maybe that will change because some part of the calculation changes. But this is the situation right now.
- jopsen 15d agoAlso not everything needs to be formal. I might want the REST API for a webshop to be solid, payment and checkout process, sure. But the UI. So long as the LLM doesn't falsify product information, why customize the layout, theme, look and feel for each and every single customer. Okay, maybe don't, but point is: you could take bigger risks, you maybe don't need to review UI changes as much.
- apsurd 15d agoThe bit about "but the UI" sounds like a developer thinking "UI is a solved problem" in the same way MBAs are told "coding is a solved problem". Product people do seem to think it worth exploring "personalized software for everyone" like literally each person gets their own custom UI. This does sound like a support mess but it's not obviously wrong when you think about the Microsoft Word alternative.
- js8 15d agoI agree LLMs are useful tools, but I am dismayed by a lot of cargo-culting around them, which happens because we don't understand them. I think we will have much better tools when we understand what is the expectation and what is the algorithm they run. Somebody else said that the magician analogy was poor. I like magic tricks, but it took many years of cultural change (influenced by people like Houdini, Randi, Penn & Teller) to stop illusionists (and mentalists) make claims they have supernatural abilities, or people believing it on their own (a magician pretending to be able to catch a bullet was shot by an audience member who didn't understand the distinction). It is detrimental, I think, to treat LLMs as if they have magical abilities ("superintelligence") rather than understanding they just run some clever algorithm. The fear for (programming) jobs comes from that framing; nobody fears of their job because of compilers, since compilers are understood. (And it actually runs against kind of "socialist" framing of the problem, which I agree with, that is why should people be worried about the jobs in the first place, when society is getting richer as a result of better tools?)
- tucnak 15d ago> It's pretty simple: due to Curry-Howard isomorphism, programming languages are just notations for some type of formal logic. Thank you, this made me chuckle!
- js8 15d agoNot really sure if it's sarcasm, but let me make a side remark. It's really stunning how much more effective the "Standard ML" notation (embraced by Haskell, Lean etc.) is compared to writing proofs in classical logic. This "UX problem" is, I think, the reason why is mathematical community embracing automated provers maybe 50 years later than they could have. Automated people wanted the better language, but the mathematicians largely resisted. So seeing this, it would be preposterous for me to think that any language, natural or not, has the last say in this. We're gonna be stuck with learning new languages and formalisms for a long time.
- ActorNightly 15d agoYour analogy is poor, and you are missing a very important fact. Most of the human written code, in places where that code needs to make money, is decidable either entirely or in large parts. I.e without running the code, you can take a domain of inputs and build a complete range of outputs solely by looking at the code. The way that works in your head is that you are effectively doing a compilation to a logical like structure, which then you can use to infer what the output will be from what the input is, and its a direct mapping that is invertible and separable, so if you know what the output should be, you know what the input is, you can pinpoint the exact location where it breaks. Thats how humans write code. If thats not clear, imagine a piece of code that splits strings by spaces, deletes the empty strings, and returns the number of words in a string. The fact that you can say that if you want 3 words, there should be maximum 2 sequences of continous spaces between words, is you effectively transpiling that program into a latent space inside your brain neurons and inverting it. LLMs essentially do this, with the added advantage of having been trained on a HUGE number of codebases, so they can recognize patterns that a human cant. Where LLMs struggle is complex behavior - they can't simulate things like a human can and choose the best course of action. Even harnesses for agentic loops that can auto run and debug code can't match what a human can do in this regard (hence why self driving still sucks rn). So moving forward, being a good coder isn't going to be about writing code, or even about prompting LLMs. Its going to be all about whether or not you can design good custom agentic loops, which necessarily involves knowledge of the model at hand (i.e what words you have to use to get it to do the right thing). This will be especially true as investment into "private" inference grows where companies will be using smaller models that have less detailed RL and thus will need much more guidance to do the right thing.
- js8 15d agoI disagree, to keep it short, what you're describing is not understanding, it's superstition. And I think it's a wrong direction of engineering, relying on some sort of irreproducible expert intuition, one that has been successfully replaced by enlightenment and scientific method. There are 3 major obstacles in understanding LLMs: 1. They use inscrutable internal language of embeddings 2. They communicate in natural language which is itself ambiguous 3. The weights and training inputs are being hidden as a "trade secret" "with the added advantage of having been trained on a HUGE number of codebases" This doesn't really mean much unless we understand what is the quality and relevance of these sources for the problem at hand. Without this understanding it's just a superstition.