4 ms·

I have a very bad opinion about this, why there were no quantum leaps in programming: in practical world there is just no time to think out of the box. its an e

I have a very bad opinion about this, why there were no quantum leaps in programming: in practical world there is just no time to think out of the box. its an endless crunch and race to ship, so something brand new and „risky“ can only be born out of strong vision and necessity. On the other hand if we take PL research - it is too far detached from practical reality. Have you ever tried grokking type proofs? It is driven by a separate breed of mathematicians that cosplay as programmers and they build their „perfect and sound“ (and useless) world. Do you know how many tons of (garbage) papers were in the era when AOP was the rage? What are the practical results? And where are they? Or take Haskell as an emple, where nobody can clearly explain to a java codemonkey what a goddamn monad is? Or endless continuations and effects research and formalisms by Felleisen and Kiselyov only for all of it be kinda rediscovered and slapped on by react devs? Useless, all of it.

anonzzzies 3y ago
Everyone can explain to everyone what a monad is for and how to use it. The fundamentals in category theory, you really don't need. But because it got such a bad name, everyone is afraid and believes it must be much harder than they think. Dependent types and other proofs are not that hard to understand in principle; you can be working on them for a very long and that indeed makes it mostly impractical. However, we will see some interesting things in search space limiting between program synthesis, verification and LLMs. I tend to prove only the parts that are vital and the things that come automatic (when the holes are automatically filled because they are already 'done').
- c_crank 3y ago
  Explaining how to use a Javascript Promise is simple. Explaining how to write idiomatic pure code using Monads is hard, and impractical in most cases, despite what FP purists will tell you.
  - anonzzzies 3y ago
    Yes, that's true, but in general programming is not easy, especially when there is something at stake (so probably most professionally written software) and as i'm work as an enterprise troubleshooter mostly in banking/insurance/trading, the depressing amounts of javascript/typescript code I encounter that should never have been put in production, while I hardly ever encounter bad f#, ocaml, rust, haskell or c++ (modern versions). Sometimes it's not excellent, but it's never as bad as the vast majority of nodejs running projects. The programmers of the latter are far more rigid, because it's hard to do anything, but when you do, you get rewarded. People learn JS in 2 days, slap on :any and blam, typescript gurus, get a job, create a system that processes millions$ and then leave for the next 'adventure'. People who invest in rigidity create better software. But yeah, they are far thinner in the 'get shit done fast' arena. So yes, I agree, if you want something done quickly and don't mind if it expires a few months later, you don't grab haskell, rust and definitely not a dependently typed language or proof assistent.
    - deleted 3y ago
      [deleted]
    - FrustratedMonky 3y ago
      Have to concur. SO many people grab Python or Javascript for a 'quick short script' and it turns into a real production system and then becomes un-maintainable. But F#, functional languages, they maybe take more time to learn, or become proficient, but the errors drop way down, because the langue doesn't allow those types of errors that are common in 'scripting' languages.
    - c_crank 3y ago
      Looks like my previous comment was too mean towards JavaScript, so trying this again... Just using some form of static typing offers easy guarantees without much effort. Trying to Monad-ify everything for a much smaller level of compiler guarantees involves much higher dev effort (as most devs do not understand Monads), and much higher effort involved in anyone reading the code.
      - anonzzzies 3y ago
  - jimbob45 3y ago
    Couldn't agree more. I wish we could replace the moniker "functional programming" with "aesthetic programming" because it feels like Monads are less practical than they are hygienic for the code.
  - vore 3y ago
    I really don't like how monads get couched in this way: they're a fundamental concept that you can see everywhere (at least understood by functional programmers with Promise.then/Promise.resolve, Array.flatMap/[x], etc.). Railing on how "using Monads is hard" makes no sense because it's a bit like talking about how using, say, Abelian groups are hard when, surprise, you use them every day.
  - bPspGiJT8Y 3y ago
    That's because monads are way more general than promises. Explaining how to use Maybe to write total functions is just as easy as explaining promises, if not easier.
    - c_crank 3y ago
      So long as you're using a single Monad like a black box. Haskell people repeatedly fail when trying to generalize them or explain the underlying premises.
kibwen 3y ago
Using Rust as an example, both the borrow checker ("region-based memory management": https://www.cs.umd.edu/projects/cyclone/papers/cyclone-regions.pdf https://www.cs.umd.edu/projects/cyclone/papers/cyclone-regio... ) and affine types were "useless" in that they failed to find any practical adoption in industry... until they suddenly weren't. Nearly the entire field of mathematics is "useless" in this way, until one day somebody accidentally invents Boolean algebra or Fourier transforms or etc. and changes the world in the process.

anonzzzies 3y ago

Everyone can explain to everyone what a monad is for and how to use it. The fundamentals in category theory, you really don't need. But because it got such a bad name, everyone is afraid and believes it must be much harder than they think. Dependent types and other proofs are not that hard to understand in principle; you can be working on them for a very long and that indeed makes it mostly impractical. However, we will see some interesting things in search space limiting between program synthesis, verification and LLMs. I tend to prove only the parts that are vital and the things that come automatic (when the holes are automatically filled because they are already 'done').

c_crank 3y ago
Explaining how to use a Javascript Promise is simple. Explaining how to write idiomatic pure code using Monads is hard, and impractical in most cases, despite what FP purists will tell you.
- anonzzzies 3y ago
  Yes, that's true, but in general programming is not easy, especially when there is something at stake (so probably most professionally written software) and as i'm work as an enterprise troubleshooter mostly in banking/insurance/trading, the depressing amounts of javascript/typescript code I encounter that should never have been put in production, while I hardly ever encounter bad f#, ocaml, rust, haskell or c++ (modern versions). Sometimes it's not excellent, but it's never as bad as the vast majority of nodejs running projects. The programmers of the latter are far more rigid, because it's hard to do anything, but when you do, you get rewarded. People learn JS in 2 days, slap on :any and blam, typescript gurus, get a job, create a system that processes millions$ and then leave for the next 'adventure'. People who invest in rigidity create better software. But yeah, they are far thinner in the 'get shit done fast' arena. So yes, I agree, if you want something done quickly and don't mind if it expires a few months later, you don't grab haskell, rust and definitely not a dependently typed language or proof assistent.
  - deleted 3y ago
    [deleted]
  - FrustratedMonky 3y ago
    Have to concur. SO many people grab Python or Javascript for a 'quick short script' and it turns into a real production system and then becomes un-maintainable. But F#, functional languages, they maybe take more time to learn, or become proficient, but the errors drop way down, because the langue doesn't allow those types of errors that are common in 'scripting' languages.
  - c_crank 3y ago
    Looks like my previous comment was too mean towards JavaScript, so trying this again... Just using some form of static typing offers easy guarantees without much effort. Trying to Monad-ify everything for a much smaller level of compiler guarantees involves much higher dev effort (as most devs do not understand Monads), and much higher effort involved in anyone reading the code.
    - anonzzzies 3y ago
- jimbob45 3y ago
  Couldn't agree more. I wish we could replace the moniker "functional programming" with "aesthetic programming" because it feels like Monads are less practical than they are hygienic for the code.
- vore 3y ago
  I really don't like how monads get couched in this way: they're a fundamental concept that you can see everywhere (at least understood by functional programmers with Promise.then/Promise.resolve, Array.flatMap/[x], etc.). Railing on how "using Monads is hard" makes no sense because it's a bit like talking about how using, say, Abelian groups are hard when, surprise, you use them every day.
- bPspGiJT8Y 3y ago
  That's because monads are way more general than promises. Explaining how to use Maybe to write total functions is just as easy as explaining promises, if not easier.
  - c_crank 3y ago
    So long as you're using a single Monad like a black box. Haskell people repeatedly fail when trying to generalize them or explain the underlying premises.

kibwen 3y ago

Using Rust as an example, both the borrow checker ("region-based memory management": https://www.cs.umd.edu/projects/cyclone/papers/cyclone-regions.pdf https://www.cs.umd.edu/projects/cyclone/papers/cyclone-regio... ) and affine types were "useless" in that they failed to find any practical adoption in industry... until they suddenly weren't. Nearly the entire field of mathematics is "useless" in this way, until one day somebody accidentally invents Boolean algebra or Fourier transforms or etc. and changes the world in the process.