361–370 of 448 posts
Earlier quoted context omitted.
And one can see how quickly they became mainstream...
I think that’s because the barrier to entry for a beginner is much higher than say python.
The quest for purity is some fountain of youth nonsense that distracts a lot of otherwise brilliant engineers.
Ask the AI to make a program that consumes a program and determine if it halts.
Earlier quoted context omitted.
> No one claims that good type systems prevent buggy software. That's exactly what languages with advanced type systems claim. To be more precise, they claim to eliminate entire classes of bugs. So they reduce bugs, they don't eliminate them completely.
If you eliminate the odd integers from consideration, you've eliminated an entire class of integers. yet, the set of remaining integers is of the same size as the original.
One example could be a low-level programming language for a given PLC manufacturer, where the prompt comes from a context-aware domain expert, and the LLM is able to output proper DSL code for that PLC. Think of "make sure this motor spins at 300rpm while this other task takes place"-type prompts.
The LLM essentially needs to juggle between understanding those highly-contextual clues, and writing DSL code that very tightly fits the DSL definition.
We're still years away from this being thoroughly reliable for all contexts, but it's interesting research nonetheless. Happy to see that someone also agrees with my sentiment ;-)
Earlier quoted context omitted.
In fact, automated regression tests done by ai with visual capabilities may have bigger impact than formal verification has. You can have an army of testers now, painfully going through every corner of your software
Will only work somewhat when customers expect features to work in a standard way. When customer spec things to work in non-standard approaches you'll just end up with a bunch of false positives.
Bug reporting is already about signal vs noise. Imagine how it will be when we hand the megaphone to bots.
Strong type systems are providing partial validation which is helping quite a lot IMO. The better we can model the state - the more constraints we can define in the model, the closer we'd be getting to writing "self-proven" code. I would assume formal proofs do way more than just ensuring validity of the model, but the similar approaches can be integrated to mainstream programs as well I believe.
Earlier quoted context omitted.
IMHO, these strong type systems are just not worth it for most tasks. As an example, I currently mostly write GUI applications for mobile and desktop as a solo dev. 90% of my time is spent on figuring out API calls and arranging layouts. Most of the data I deal with are strings with their own validation and formatting rules that are complicated and at the same time usually need to be permissive. Even at the backend a…
> Most of the data I deal with are strings with their own validation and formatting rules that are complicated and at the same time usually need to be permissive this is exactly where a good type system helps: you have an unvalidated string and a validated string which you make incompatible at the type level, thus eliminating a whole class of possible mistakes. same with object ids, etc. don't need haskell for this,…
Earlier quoted context omitted.
> No one claims that good type systems prevent buggy software. But, they do seem to improve programmer productivity. To me it seems they reduce productivity. In fact, for Rust, which seems to match the examples you gave about locks or regions of memory the common wisdom is that it takes longer to start a project, but one reaps the benefits later thanks to more confidence when refactoring or adding code. However, even…
> In my experience, the more information is encoded in the type system, the more effort is required to change code. I would tend to disagree. All that information encoded in the type system makes explicit what is needed in any case and is otherwise only carried informally in peoples' heads by convention. Maybe in some poorly updated doc or code comment where nobody finds it. Making it explicit and compiler-enforced i…
this is, in fact better for llms, they are better at carrying information and convention in their kv cache than they are in having to figure out the actual types by jumping between files and burning tokens in context/risking losing it on compaction (or getting it wrong and having to do a compilation cycle).
if a typed language lets a developer fearlessly build a semantically inconsistent or confusing private API, then llms will perform poorer at them even though correctness is more guaranteed.
I don't think formal verification really addresses most day-to-day programming problems: * A user interface is confusing, or the English around it is unclear * An API you rely on changes, is deprecated, etc. * Users use something in unexpected ways * Updates forced by vendors or open source projects cause things to break * The customer isn't clear what they want * Complex behavior between interconnected systems, out…
> But I don't think that represents a lot of what most of us are tasked with Give me a list of all the libraries you work with that don't have some sort of "okay but not that bit" rule in the business logic, or "all of those function are f(src, dst) but the one you use most is f(dst,src) and we can't change it now". I bet it's a very short list. Really we need to scrap every piece of software ever written and start a…
Earlier quoted context omitted.
There’s two types of slowdown at play: a) It’s fast to change the code, but now I have failures in some apparently unrelated part of the code base. (Javascript) and fixing that slows me down. b) It’s slow to change the code because I have to re-encode all the relationships and semantic content in the type system (Rust), but once that’s done it will likely function as expected. Depending on project, one or the other i…
Or: I’m not going to do this refactor at all, even though it would improve the codebase, because it will be near impossible to ensure everything is correct after making so many changes. To me, this has been one of the biggest advantages of both tests and types. They provide confidence to make changes without needing to be scared of unintended breakages.