5 ms·

A limited form of formal verification is already mainstream. It is called type systems. The industry in general has been slowly moving to encode more invariants

• devin 10mo ago
  > No one claims that good type systems prevent buggy software. But, they do seem to improve programmer productivity. They really don’t. How did you arrive at such a conclusion?
  • mplewis 10mo ago
    Through empirical evidence? Do you think that the vast majority of software devs moved to typing for no reason?
    • avmich 10mo ago
      It's a bad reason. A lot of best practices are temporary blindnesses, comparable, in some sense, with supposed love to BASIC before or despite Dijkstra. So, yes, it's possible there is no good reason. Though I don't think it's the case here.
    • wolvesechoes 10mo ago
      > Do you think that the vast majority of software devs moved to typing for no reason? It is quite clear that this industry is mostly driven by hype and fades, not by empirical studies. Empirical evidence in favor of a claim that static typing and complex type systems reduce bugs or improve productivity is highly inconclusive at best
    • gf000 10mo ago
      We don't actually have empirical evidence on the topic, surprisingly. It's just people's hunches.
      • JumpCrisscross 10mo ago
        I feel like the terms logical, empirical, rational and objective are used interchangeably by the general public, with one being in vogue at a time.
  • Permik 10mo ago
    Not that I can answer for OP but as a personal anecdote; I've never been more productive than writing in Rust, it's a goddamn delight. Every codebase feels like it would've been my own and you can get to speed from 0 to 100 in no time.
    • leoedin 10mo ago
      Yeah, I’ve been working mainly in rust for the last few years. The compile time checks are so effective that run time bugs are rare. Like you can refactor half the codebase and not run the app for a week, and when you do it just works. I’ve never had that experience in other languages.
• kreetx 10mo ago
  Some type systems (e.g, Haskell) are closing in in becoming formal verification languages themselves.
  • rixed 10mo ago
    And one can see how quickly they became mainstream...
    • egwor 10mo ago
      I think that’s because the barrier to entry for a beginner is much higher than say python.
      • qrobit 10mo ago
        I would argue that the barrier to entry is on par with python for a person with no experience, but you need much more time with Haskell to become proficient in it. In python, on the other hand, you can learn the basics and these will get you pretty far
      • jonathanstrange 10mo ago
        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 all the data is in the end converted to strings and integers when it is put into a database. Over-the-wire serialization also discards with most typing (although I prefer protocol buffers to alleviate this problem a bit). Strong typing can be used in between those steps but the added complexity from data conversions introduces additional sources of error, so in the end the advantages are mostly nullified.
        • baq 10mo ago
          > 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, either: https://brightinventions.pl/blog/branding-flavoring/ https://brightinventions.pl/blog/branding-flavoring/
• blub 10mo ago
  > 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 that weaker claim hasn’t been proven. In my experience, the more information is encoded in the type system, the more effort is required to change code. My initial enthusiasm for the idea of Ada and Spark evaporated when I saw how much ceremony the code required.
  • teiferer 10mo ago
    > 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 is a good thing. It might feel like a burden at first, but you're otherwise just closing your eyes and ignoring what can end up important. Changed assumptions are immediately visible. Formal verification just pushes the boundary of that.
    • blub 10mo ago
      In practice it would be encoded in comments, automated tests and docs, with varying levels of success. It’s actually similar to tests in a way: they provide additional confidence in the code, but at the same time ossify it and make some changes potentially more difficult. Interestingly, they also make some changes easier, as long as not too many types/tests have to be adapted.
      • gf000 10mo ago
        Constraints Liberate, Liberties Constrain. (I also recommend watching the presentation with the same title)
      • 10mo ago
• elbear 10mo ago
  > 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.
  • bonesss 10mo ago
    No nulls, no nullability bombs. Forcing devs to pre-fix/avoid bugs before the compiler will allow the app means the programs are more correct as a group. Wrong, incomplete, insufficient, unhelpful, unimpressive, and dumb are all still very possible. But more correct than likely in looser systems.
    • fc417fc802 10mo ago
      > No nulls, no nullability bombs. I hate this meme. Null indicates something. If you disallow null that same state gets encoded in some other way. And if you don't properly check for that state you get the exact same class of bug. The desirable type system feature here is the ability to statically verify that such a check has occurred every time a variable is accessed. Another example is bounds checking. Languages that stash the array length somewhere and verify against it on access eliminate yet another class of bug without introducing any programmer overhead (although there generally is some runtime overhead).
      • yencabulator 10mo ago
        The whole point of "no nullability bombs" is to make it obvious in the type system when the value might be not present, and force that to be handled. Javascript: let x = foo(); if (x.bar) { ... } // might blow up Typescript: let x = foo(); // type of x is Foo | undefined if (x === undefined) { ...; return; } // I am forced to handle this if (x.bar) { ... } // this is now safe, as Typescript knows x can only be a Foo now (Of course, languages like Rust do that cleaner, since they don't have to be backwards-compatible with old Javascript. But I'm using Typescript in hopes of a larger audience.)
  • 10mo ago
• skissane 10mo ago
  > For LLMs, there is an added benefit. If you can formally specify what you want, you can make that specification your entire program. Then have an LLM driven compiler produce a provably correct implementation. This is a novel programming paradigm that has never before been possible; although every "declarative" language is an attempt to approximate it. The problem is there is always some chance a coding agent will get stuck and be unable to produce a conforming implementation in a reasonable amount of time. And then you are back in a similar place to what you were with those pre-LLM solutions - needing a human expert to work out how to make further progress.
  • GTP 10mo ago
    With the added issue that now the expert is working with code they didn't write, and that could be in general be harder to understand than human-written code. So they could find it easier to just throw it away and start from scratch.
• Marazan 10mo ago
  > For LLMs, there is an added benefit. If you can formally specify what you want, you can make that specification your entire program. Then have an LLM driven compiler produce a provably correct implementation. This is a novel programming paradigm that has never before been possible; although every "declarative" language is an attempt to approximate it. That is not novel and every declarative language precisely embodies it.
  • naasking 10mo ago
    I think most existing declarative languages still require the programmer to specify too many details to get something usable. For instance, Prolog often requires the use of 'cut' to get reasonable performance for some problems.
• YouAreWRONGtoo 10mo ago
  [dead]