4 ms·

For the working programmer do you really want theoretical soundness? Though I have background in formal mathematics, when it comes to day to day, and what pays

For the working programmer do you really want theoretical soundness? Though I have background in formal mathematics, when it comes to day to day, and what pays the bills, what I might need to operate in anger, I much much more care about legibility, debuggability, inspectability, easy to implement X (without a stdlib if need be), easy to test, no footguns, PL respects programmers (btw go fails most of these)

cyberpunk 4y ago
In my experience go is great at all of these, but then again I’m coming from c and then erlang…
ratww 4y ago
I personally do. At my company we recently finished adding types to some libraries that were a core part of our system but were deemed "untypeable" by the maintainers of the libraries themselves (we're contributing back), and only band-aids existed. We needed several advanced typing features in our languages for that that weren't available for us a couple years ago. Each time we added more advanced typing to new sections of the system, new bugs and security issues were found. At the end there were over 100 places that were being used incorrectly. This is something that linters and the library itself failed to catch for years, but with proper typing we got there.
- throwawaymaths 4y ago
  That's not theoretical soundness, that's actual correctness. I'm mostly talking about things like io monads.
  - ratww 4y ago
    I don't see why you're assuming we did something different, I even said "advanced typing features". We have several effect-related types, including IO.
  - hither_shores 4y ago
    If your code can run IO operations synchronously and branch on the result of previous operations, you've already got an IO monad. The point of being explicit about that is that it allows you to check that a given piece of code can't do those things. Keeping database calls out of the render loop, for instance, is very much a matter of actual correctness.
    - throwawaymaths 4y ago
      In most languages with an io monads your power of proving that x can or can't be done comes at the cost of hiding the business data inside of the monad type (that wraps it) which severely impacts debuggability and in many cases, code legibility and understandability of the data you care about -- because there might be a business logic error elsewhere that you need to track down that no amount of formal correctness will save you from.
      - ratww 4y ago
        The decades-old solution for that is to not mix the business and IO code in the first place. If you do, that's entirely on you. This works exactly the same and has the same goals as in popular OOP architectural patterns like Clean Architecture, Hexagonal Architecture or Onion Architecture. With the difference that with a better type system it becomes significantly harder to do this kinda thing to begin with, and that's a GREAT thing. Your business code is extremely simple, reusable, isn't intertwined with IO stuff and is 100% testable with minimal effort, without needing mocks or anything of the sort. If you don't care about this kind of correctness, then fine, but don't pretend this is something that's not sought after by both OOP and FP practitioners.
        throwawaymaths 4y ago
        Where did you get the idea that I practice oop? I exclusively use FP, and I use hexagonal-ish fp design. But question. Suppose you discover you have a logic bug and you write a pure logic test for it. But perhaps the path through the business logic was written by someone else, who has since left the company. It's a tax rule so you have to navigate through several layers of abstractions that are sometimes specialized for different countries, sometimes generalized. Maybe they didn't write all the tests that you'd like to see. You have one hour to deploy a patch because 9-5 customers are entering their work hours on a different continent whose tax rules are what you need to fix. How do you introspect the data that are moving through the code?

cyberpunk 4y ago

In my experience go is great at all of these, but then again I’m coming from c and then erlang…

ratww 4y ago

I personally do. At my company we recently finished adding types to some libraries that were a core part of our system but were deemed "untypeable" by the maintainers of the libraries themselves (we're contributing back), and only band-aids existed. We needed several advanced typing features in our languages for that that weren't available for us a couple years ago. Each time we added more advanced typing to new sections of the system, new bugs and security issues were found. At the end there were over 100 places that were being used incorrectly. This is something that linters and the library itself failed to catch for years, but with proper typing we got there.

throwawaymaths 4y ago
That's not theoretical soundness, that's actual correctness. I'm mostly talking about things like io monads.
- ratww 4y ago
  I don't see why you're assuming we did something different, I even said "advanced typing features". We have several effect-related types, including IO.
- hither_shores 4y ago
  If your code can run IO operations synchronously and branch on the result of previous operations, you've already got an IO monad. The point of being explicit about that is that it allows you to check that a given piece of code can't do those things. Keeping database calls out of the render loop, for instance, is very much a matter of actual correctness.
  - throwawaymaths 4y ago
    In most languages with an io monads your power of proving that x can or can't be done comes at the cost of hiding the business data inside of the monad type (that wraps it) which severely impacts debuggability and in many cases, code legibility and understandability of the data you care about -- because there might be a business logic error elsewhere that you need to track down that no amount of formal correctness will save you from.
    - ratww 4y ago
      The decades-old solution for that is to not mix the business and IO code in the first place. If you do, that's entirely on you. This works exactly the same and has the same goals as in popular OOP architectural patterns like Clean Architecture, Hexagonal Architecture or Onion Architecture. With the difference that with a better type system it becomes significantly harder to do this kinda thing to begin with, and that's a GREAT thing. Your business code is extremely simple, reusable, isn't intertwined with IO stuff and is 100% testable with minimal effort, without needing mocks or anything of the sort. If you don't care about this kind of correctness, then fine, but don't pretend this is something that's not sought after by both OOP and FP practitioners.
      - throwawaymaths 4y ago
        Where did you get the idea that I practice oop? I exclusively use FP, and I use hexagonal-ish fp design. But question. Suppose you discover you have a logic bug and you write a pure logic test for it. But perhaps the path through the business logic was written by someone else, who has since left the company. It's a tax rule so you have to navigate through several layers of abstractions that are sometimes specialized for different countries, sometimes generalized. Maybe they didn't write all the tests that you'd like to see. You have one hour to deploy a patch because 9-5 customers are entering their work hours on a different continent whose tax rules are what you need to fix. How do you introspect the data that are moving through the code?