5 ms·

With a sufficiently advanced type system, you could lay out high level building blocks, such as function definitions, and let the LLM go wild, and then if thing

With a sufficiently advanced type system, you could lay out high level building blocks, such as function definitions, and let the LLM go wild, and then if things compile there's a high chance it's correct. Or maybe even a formal proof things are correct. I was blown away when I realized some Haskell functions have only one possible definition, for example. I think most people haven't worked with type systems like this, and there are type systems far more powerful than Haskell's, such as dependant types. There's not much reason to worry about low level quality standards so long as you know it's correct from a high level. I don't think we've seen what a deep integration between a LLM and a programming language can do, where the type system helps validate the LLM output, and the LLM has a type checker integrated into its training process.

fhdsgbbcaA 2y ago
Things I never want to hear about flight control systems before I board a plane: “if things compile there's a high chance it's correct”
- literalAardvark 2y ago
  Very odd comment, since that's exactly what you do want to hear
  - xmprt 2y ago
    There's a lot of code that compiles but isn't correct.
    - literalAardvark 2y ago
      Because we're using languages with flexibility but no correctness, but the vast performance advantage AI programming has over us could be used to manage the formal proofs for a verified toolchain. We're not quite there yet, but while regular programming is quite tough for AI due to how fuzzy it is, formal proofs are something AI is already very good at.
  - gloflo 2y ago
    I'd rather hear: "The compiled code has gone through all tests in the comprehensive, human-expert-written, standardized test suite correctly" Compiling does not differentiate between True and False, so no safety for that escape pod door.
    - literalAardvark 2y ago
      I took that as part of the build process. But I definitely want as much as possible to be automated and formally correct, which is why I wrote what I wrote.
  - ziggyzecat 2y ago
    if-then-high-chance logic is for sex education & prototypes, not for airplanes carrying insured passengers
halfmatthalfcat 2y ago
I'm not sure how much things have changed but I tried to use GPT-4 when it first came out to build a library on top of Scala + Shapeless and it utterly failed. Unless you can somehow wire in an LSP per language as an agent and have it work through the type errors as it tries to create code, I can't see where we'll ever get to a place where LLMs can work with strongly typed languages and produce compliant code. Even with, the aforementioned "have an LSP agent work through type errors", it may be faster to just do it yourself than wait for an LLM to spit out what may be correct.
- nycdatasci 2y ago
  Definitely try Claude 3.5 Sonnet and o1-preview. They have succeeded for me where other models have failed. Also, use Cursor IDE.
  - cft 2y ago
    o1-mini is even higher in coding benchmarks than o1-preview. That has been my experience also.
  - mlhpdx 2y ago
    Oh, I’ve found Claude 3.5 to be better but still pointless. To be specific, it generates code that does what I ask (roughly) but… - Has obvious bugs, many at runtime - Has subtle bugs. - Is inefficient. All of which it will generally fix when asked. But how useful is it if I need to know all the problems with its code beforehand? Then it responds with the same-ish wrong answer the next time. Still a long way to go IMO.
  - csomar 2y ago
    Claude 3.5 is good, however, it's "Type comprehension" is really basic. That was my experience with it when using Rust. It still can't create an internal mental model of the types and how to link them together. It'll also, at some points, start to heavily hallucinate functions and stuff.
- tharant 2y ago
  Glad to know I’m not the only one who has had difficulties getting reasonable Scala code from an LLM. While I agree that LSP integration would likely help with generating or debugging production-quality code, I’d also suggest that the need for an LSP demonstrates these models’ inability to reason—at least about code. Perhaps they were trained more deeply and carefully on the marketing or “getting started” pages for the libraries and languages I need to use and not as much on examples of production-quality code repositories that make use of those languages/libs/tools.
oblio 2y ago
> With a sufficiently advanced type system Is this a brother or a cousin of the "sufficiently advanced compiler"? :-)
- MichaelBurge 2y ago
  Anything on top of the Calculus of Constructions is usually enough. So it's not a moving target, and there are multiple implementations.
- inopinatus 2y ago
  if there is only one valid translation of the type constraints into executable code then what you have is a slow, expensive, and occasionally argumentative compiler it merely remains to build a debugger for your Turing-complete type system, and the toolchain will be ready for production
- zahlman 2y ago
  A component, if I correctly understand the proponents of such type systems.
- tessierashpool9 2y ago
  it certainly is a sister or niece of the "sufficiently advanced technology".
- Buttons840 2y ago
  > Is this a brother or a cousin of the "sufficiently advanced compiler"? :-) I believe the claim was that a sufficiently advanced compiler could do a lot of optimization and greatly improve performance. Maybe my claim here will turn out the same.
skybrian 2y ago
The functions for which there's only one implementation are trivial examples. It's not going to work for anything even slightly more complicated, like a function that returns a float. Even if you could, you probably wouldn't want to make any change a breaking change by exposing implementation details.
rapind 2y ago
Oh this is an interesting take. Haskell, F#, possibly Elm, etc.
TechDebtDevin 2y ago
I'm sort of playing around with something like this in go for fun.
szundi 2y ago
You know people work with what they work with.
rq1 2y ago
I did just that actually to: * build a codegen for Idris2 and a rust RT (a parallel stack "typed" VM) * a full application in Elm, while asking it to borrow from DT to have it "correct-by-construction", use zippers for some data structures… etc. And it worked! * Whilst at it, I built Elm but in Idris2, while improving on the rendering part (this is WIP) * data collators and iterators to handle some ML trainings with pausing features so that I can just Ctrl-C and continue if needed/possible/makes sense. * etc. At the end I had to rewrite completely some parts, but I would say 90% of the boring work was correctly done and I only had to focus on the interesting bits. However it didn’t deliver the kind of thorough prep work a painter would do before painting a house when asked for. It simply did exactly what I asked, meaning, it did the paint and no more. (Using 4o and o1-preview)
- anonzzzies 2y ago
  any code to see? I like Idris so this would be interesting.
- tharant 2y ago
  I keep seeing folks who say they’ve built a “full application” using or deeply collaborating with an LLM but, aside from code that is only purported to be LLM-generated, I’ve yet to see any evidence that I can consider non-trivial. Show me the chat sessions that produced these “full applications”.
  - simonw 2y ago
    How about this one? https://simonwillison.net/2024/Mar/30/ocr-pdfs-images/ https://simonwillison.net/2024/Mar/30/ocr-pdfs-images/ That's for this: https://tools.simonwillison.net/ocr https://tools.simonwillison.net/ocr
    - tharant 2y ago
      An application powered by a single source file comprised of only 400 lines of code is, by my definition, trivial. My needs are more complex than that, and I’d expect that the vast majority of folks who are trying to build or maintain production quality revenue generating code have the same or similar needs. Again, please don’t be offended; what you’re doing is great and I dearly appreciate you sharing your experience! Just be aware that the stuff you’re demonstrating isn’t (hasn’t been, for me at least) capable of producing the kind of complexity I need while using the languages and tooling required in my environment. In other words, while everything of yours I’ve seen has intellectual and perhaps even monetary value, that doesn’t mean your examples or strategies work for all use-cases.
runeks 2y ago
> With a sufficiently advanced type system, you could lay out high level building blocks, such as function definitions, and let the LLM go wild, and then if things compile there's a high chance it's correct. Or maybe even a formal proof things are correct. A formal proof is simply a type that allows only the correct implementation at the term level. And specifying this takes ages, as in hundreds of times longer than just writing it out. So you want to use an LLM to save this 1% of time after you've done all the hard work of specifying what the only correct implementation is?
gabigrin 2y ago
That's one take I'm trying to take with https://www.flyde.dev https://www.flyde.dev. Build that higher-level abstraction that allows LLM to shine and us humans to enjoy a more effective way to view and control its outcome. I know it's not what you meant, but tbh I don't think going deeper than Haskell on type-system power is the route to achieve mass adoption.

fhdsgbbcaA 2y ago

Things I never want to hear about flight control systems before I board a plane: “if things compile there's a high chance it's correct”

literalAardvark 2y ago
Very odd comment, since that's exactly what you do want to hear
- xmprt 2y ago
  There's a lot of code that compiles but isn't correct.
  - literalAardvark 2y ago
    Because we're using languages with flexibility but no correctness, but the vast performance advantage AI programming has over us could be used to manage the formal proofs for a verified toolchain. We're not quite there yet, but while regular programming is quite tough for AI due to how fuzzy it is, formal proofs are something AI is already very good at.
- gloflo 2y ago
  I'd rather hear: "The compiled code has gone through all tests in the comprehensive, human-expert-written, standardized test suite correctly" Compiling does not differentiate between True and False, so no safety for that escape pod door.
  - literalAardvark 2y ago
    I took that as part of the build process. But I definitely want as much as possible to be automated and formally correct, which is why I wrote what I wrote.
- ziggyzecat 2y ago
  if-then-high-chance logic is for sex education & prototypes, not for airplanes carrying insured passengers

halfmatthalfcat 2y ago

I'm not sure how much things have changed but I tried to use GPT-4 when it first came out to build a library on top of Scala + Shapeless and it utterly failed. Unless you can somehow wire in an LSP per language as an agent and have it work through the type errors as it tries to create code, I can't see where we'll ever get to a place where LLMs can work with strongly typed languages and produce compliant code. Even with, the aforementioned "have an LSP agent work through type errors", it may be faster to just do it yourself than wait for an LLM to spit out what may be correct.

nycdatasci 2y ago
Definitely try Claude 3.5 Sonnet and o1-preview. They have succeeded for me where other models have failed. Also, use Cursor IDE.
- cft 2y ago
  o1-mini is even higher in coding benchmarks than o1-preview. That has been my experience also.
- mlhpdx 2y ago
  Oh, I’ve found Claude 3.5 to be better but still pointless. To be specific, it generates code that does what I ask (roughly) but… - Has obvious bugs, many at runtime - Has subtle bugs. - Is inefficient. All of which it will generally fix when asked. But how useful is it if I need to know all the problems with its code beforehand? Then it responds with the same-ish wrong answer the next time. Still a long way to go IMO.
- csomar 2y ago
  Claude 3.5 is good, however, it's "Type comprehension" is really basic. That was my experience with it when using Rust. It still can't create an internal mental model of the types and how to link them together. It'll also, at some points, start to heavily hallucinate functions and stuff.
tharant 2y ago
Glad to know I’m not the only one who has had difficulties getting reasonable Scala code from an LLM. While I agree that LSP integration would likely help with generating or debugging production-quality code, I’d also suggest that the need for an LSP demonstrates these models’ inability to reason—at least about code. Perhaps they were trained more deeply and carefully on the marketing or “getting started” pages for the libraries and languages I need to use and not as much on examples of production-quality code repositories that make use of those languages/libs/tools.

oblio 2y ago

> With a sufficiently advanced type system Is this a brother or a cousin of the "sufficiently advanced compiler"? :-)

MichaelBurge 2y ago
Anything on top of the Calculus of Constructions is usually enough. So it's not a moving target, and there are multiple implementations.
inopinatus 2y ago
if there is only one valid translation of the type constraints into executable code then what you have is a slow, expensive, and occasionally argumentative compiler it merely remains to build a debugger for your Turing-complete type system, and the toolchain will be ready for production
zahlman 2y ago
A component, if I correctly understand the proponents of such type systems.
tessierashpool9 2y ago
it certainly is a sister or niece of the "sufficiently advanced technology".
Buttons840 2y ago
> Is this a brother or a cousin of the "sufficiently advanced compiler"? :-) I believe the claim was that a sufficiently advanced compiler could do a lot of optimization and greatly improve performance. Maybe my claim here will turn out the same.

skybrian 2y ago

The functions for which there's only one implementation are trivial examples. It's not going to work for anything even slightly more complicated, like a function that returns a float. Even if you could, you probably wouldn't want to make any change a breaking change by exposing implementation details.

rapind 2y ago

Oh this is an interesting take. Haskell, F#, possibly Elm, etc.

TechDebtDevin 2y ago

I'm sort of playing around with something like this in go for fun.

szundi 2y ago

You know people work with what they work with.

rq1 2y ago

I did just that actually to: * build a codegen for Idris2 and a rust RT (a parallel stack "typed" VM) * a full application in Elm, while asking it to borrow from DT to have it "correct-by-construction", use zippers for some data structures… etc. And it worked! * Whilst at it, I built Elm but in Idris2, while improving on the rendering part (this is WIP) * data collators and iterators to handle some ML trainings with pausing features so that I can just Ctrl-C and continue if needed/possible/makes sense. * etc. At the end I had to rewrite completely some parts, but I would say 90% of the boring work was correctly done and I only had to focus on the interesting bits. However it didn’t deliver the kind of thorough prep work a painter would do before painting a house when asked for. It simply did exactly what I asked, meaning, it did the paint and no more. (Using 4o and o1-preview)

anonzzzies 2y ago
any code to see? I like Idris so this would be interesting.
tharant 2y ago
I keep seeing folks who say they’ve built a “full application” using or deeply collaborating with an LLM but, aside from code that is only purported to be LLM-generated, I’ve yet to see any evidence that I can consider non-trivial. Show me the chat sessions that produced these “full applications”.
- simonw 2y ago
  How about this one? https://simonwillison.net/2024/Mar/30/ocr-pdfs-images/ https://simonwillison.net/2024/Mar/30/ocr-pdfs-images/ That's for this: https://tools.simonwillison.net/ocr https://tools.simonwillison.net/ocr
  - tharant 2y ago
    An application powered by a single source file comprised of only 400 lines of code is, by my definition, trivial. My needs are more complex than that, and I’d expect that the vast majority of folks who are trying to build or maintain production quality revenue generating code have the same or similar needs. Again, please don’t be offended; what you’re doing is great and I dearly appreciate you sharing your experience! Just be aware that the stuff you’re demonstrating isn’t (hasn’t been, for me at least) capable of producing the kind of complexity I need while using the languages and tooling required in my environment. In other words, while everything of yours I’ve seen has intellectual and perhaps even monetary value, that doesn’t mean your examples or strategies work for all use-cases.

runeks 2y ago

> With a sufficiently advanced type system, you could lay out high level building blocks, such as function definitions, and let the LLM go wild, and then if things compile there's a high chance it's correct. Or maybe even a formal proof things are correct. A formal proof is simply a type that allows only the correct implementation at the term level. And specifying this takes ages, as in hundreds of times longer than just writing it out. So you want to use an LLM to save this 1% of time after you've done all the hard work of specifying what the only correct implementation is?

gabigrin 2y ago

That's one take I'm trying to take with https://www.flyde.dev https://www.flyde.dev. Build that higher-level abstraction that allows LLM to shine and us humans to enjoy a more effective way to view and control its outcome. I know it's not what you meant, but tbh I don't think going deeper than Haskell on type-system power is the route to achieve mass adoption.