5 ms·

I like that things like this exist even if I recognize that they are not for me. For some class of system I am sure these languages will shine. It reminds me of

I like that things like this exist even if I recognize that they are not for me. For some class of system I am sure these languages will shine. It reminds me of Julia - every time I come across it I love the idea of it but I have no personal use for it. I'm always interested in reading articles on dependent type languages like Coq and Idris but I haven't even tried to write a "Hello, World!" in them. I may just be jaded with promises of sufficiently smart compilers. I actually hold out more hope for AI code assistance than I do for easy-to-use formal verification. It is a bit like Esperanto or something like that. Maybe I am just brain damaged from growing up in a world with English and other messy spoken languages but my intuition suggests that perfectly structured languages are possibly the wrong approach. Even though at the time I wanted xhtml to win the battle of structured formats for the web, in hindsight I now believe messy html 5 was the way to go. > We still get buffer overflows and integer overflows. The compiler still cannot tell when our loops will terminate (yes, this is possible). Aliasing is still a complete unbridled mess. As strange as it sounds, I've learned to love the flaws. I don't see my job in life is to remove every possible source of error. There seems to be a balance point where the cure is worse than the disease and I wish to find that balance point rather than some theoretical perfect. So I do hate those things listed. But so far, the balance point for me is with languages that sacrifice perfectly solving those problems.

nine_k 3y ago
Highly regular natural languages exist and thrive. I'd say that Japanese is a way, way more regularly structured language than English. Loving flaws like buffer overflows looks more like a Stockholm syndrome to me: when the reality is terrible, people learn to find lovable bits in it, just to avoid insanity. C has its place, but its place is very, very close to hardware. (And I hope Zig will push it from there, too, eventually.) I don't think that better static guarantees are going to come from direct adoption of languages like Haskell, or some tools like Coq or Agda. They will continue coming the same way Rust and Typescript gone mainstream: by integrating them into practical (not research) languages, and allowing escape hatches, prominently marked. Advanced features need adaptation to be ergonomic, after that they feel natural. This happens to every scientific achievement that has a large practical value: compare a laser on an optical workbench in a lab to a laser in a DVD drive, or a laser pointer. I would likely laugh if someone told me in 1995 that pure FP approaches will conquer GUI development. Nevertheless, this happened twice: first with XSLT in 2000s, then with React in 2010s.
- eindiran 3y ago
  It's funny that you picked the language with the single worst and most fundamentally broken orthographic system in the world as your example.
- valenterry 3y ago
  react is not an example for a library that is supposed to be or even possible to be used in a pure functional programming way.
  - adamwk 3y ago
    Right, there's definitely functional-inspired bones (e.g., a view is a function of state); but every hook is a side effect, even the redux ones. And I don't think it would even be improved by being pure; Elm has much more boilerplate to do similar things.
    - valenterry 3y ago
      haha, Adam from SM, is it you?
  - WorldMaker 3y ago
    React can still be viewed as functional programming if you assume Hooks operate in/on/with an unnamed/untyped monad. ("Pure" of course depends on your take of monadic programming from there.) It might be nice if that monad were better typed and/or at least parametric (reflected in input or output parameters), but it all exists in an untyped language to begin with, so it is mostly fine how it works right now. Mostly.
    - valenterry 3y ago
      I don't know. I haven't used hooks much, but while you might consider it pure-functional in a way within a component that uses (a single) hook, I think using multiple hooks and having everything integrated is certainly not pure-functional. It's easy to test right? Can you replace calls/expressions with their result-value? If no, it's not pure-functional.
dunham 3y ago
The dependent languages are interesting. But the theorem proving is not easy, and probably overkill for a lot of applications. Even for stuff like boundary conditions for binary search, which could be checked with Hoare logic, I usually handle by stealing the implementation from the Go standard library (so I don't have to think about it). Last year I did advent of code in Lean4. I had written a heap implementation that I didn't end up using. As an exercise, I went back and added proofs for my indicies and a termination proof. I got the termination proof down to `0 < 0` and realized that I had an off by one error (I'd used the math for a 1-based array with a 0-based array). My take-away was that this stuff can catch real bugs, but also that people are not going to do this stuff day-to-day. Maybe some equality saturation thing will make it possible for the compiler to sort out the proof in most cases. If the compiler can hit 80%, you could use it as a linter. (If you want something stricter, you can do totality checking but have escape hatches like Idris' assert_total / assert_smaller.) > Even though at the time I wanted xhtml to win the battle of structured formats for the web, in hindsight I now believe messy html 5 was the way to go. The structured vs unstructured thing is also interesting. I came to a similar conclusion years ago. I'd written some heuristics to pull recipes out of web pages, and also use embedded microdata on some pages. I found I got better results with my heuristics because of bad encoding of the structured data. E.g. a web site was missing entire ingredient blocks in their encoding because their process / data model didn't accommodate recipes with multiple ingredient blocks.
deleted 3y ago
[deleted]
PsylentKnight 3y ago
> It is a bit like Esperanto or something like that. Maybe I am just brain damaged from growing up in a world with English and other messy spoken languages but my intuition suggests that perfectly structured languages are possibly the wrong approach. You seem to be implying Esperanto's lack of popularity is related to its regularity, but I don't think it has anything to do with that - it comes down to network effects. It's not an official language in any country. There are very, very few native speakers of Esperanto. Of those blessed few, they obviously have at least one other native language, otherwise they'd be completely cut off from society. And by the same token, English is popular as a second language due to network effects and the benefits learning it can confer (read: better economic opportunities) and little to do with its regularity. A lot of people have had the experience of learning a bit of Spanish and realizing that English's spelling system is atrociously irregular and we gain nothing by having so many spelling rules that have so many exceptions they can hardly be considered "rules". In fact, English's spelling used to be much more regular, it's just that our pronunciations have shifted a lot over time while the spelling has remained relatively static. This is all tangential to your larger point, I just like talking about this kind of thing.
thr_ddv 3y ago
>The compiler still cannot tell when our loops will terminate (yes, this is possible). while(n < busy_bever(10)) n++ Tell me when my loop terminates.
- littlestymaar 3y ago
  That's not a very good exemple because with BB we know the code terminates, by definition. The canonical tong-in-cheek argument is to use the Collatz conjoncture instead (but even that isn't a good example in practice: https://news.ycombinator.com/item?id=21440306 https://news.ycombinator.com/item?id=21440306)
  - thr_ddv 3y ago
    I'm not asking if it terminates, I'm asking when it does. After all it's not much use if the number overflows the universe.
    - littlestymaar 3y ago
      But that's not something these kinds of tools are supposed do, even with trivial functions… These tools have no idea about the run-time (and there's no way they coule, since it depends on the load you put on the hardware in parallel of running your program)
      - redjamjar 3y ago
        I agree. There are tools though which are specifically for determining worst-case execution time for e.g. embedded systems which can actually give accurate timing information (upto a point).
    - redjamjar 3y ago
      Yeah, so these tools will not tell you how long it will take to terminate --- only that it will eventually. In the vast majority of cases, that is what you want to know.
    - 3y ago

nine_k 3y ago

Highly regular natural languages exist and thrive. I'd say that Japanese is a way, way more regularly structured language than English. Loving flaws like buffer overflows looks more like a Stockholm syndrome to me: when the reality is terrible, people learn to find lovable bits in it, just to avoid insanity. C has its place, but its place is very, very close to hardware. (And I hope Zig will push it from there, too, eventually.) I don't think that better static guarantees are going to come from direct adoption of languages like Haskell, or some tools like Coq or Agda. They will continue coming the same way Rust and Typescript gone mainstream: by integrating them into practical (not research) languages, and allowing escape hatches, prominently marked. Advanced features need adaptation to be ergonomic, after that they feel natural. This happens to every scientific achievement that has a large practical value: compare a laser on an optical workbench in a lab to a laser in a DVD drive, or a laser pointer. I would likely laugh if someone told me in 1995 that pure FP approaches will conquer GUI development. Nevertheless, this happened twice: first with XSLT in 2000s, then with React in 2010s.

eindiran 3y ago
It's funny that you picked the language with the single worst and most fundamentally broken orthographic system in the world as your example.
valenterry 3y ago
react is not an example for a library that is supposed to be or even possible to be used in a pure functional programming way.
- adamwk 3y ago
  Right, there's definitely functional-inspired bones (e.g., a view is a function of state); but every hook is a side effect, even the redux ones. And I don't think it would even be improved by being pure; Elm has much more boilerplate to do similar things.
  - valenterry 3y ago
    haha, Adam from SM, is it you?
- WorldMaker 3y ago
  React can still be viewed as functional programming if you assume Hooks operate in/on/with an unnamed/untyped monad. ("Pure" of course depends on your take of monadic programming from there.) It might be nice if that monad were better typed and/or at least parametric (reflected in input or output parameters), but it all exists in an untyped language to begin with, so it is mostly fine how it works right now. Mostly.
  - valenterry 3y ago
    I don't know. I haven't used hooks much, but while you might consider it pure-functional in a way within a component that uses (a single) hook, I think using multiple hooks and having everything integrated is certainly not pure-functional. It's easy to test right? Can you replace calls/expressions with their result-value? If no, it's not pure-functional.

dunham 3y ago

The dependent languages are interesting. But the theorem proving is not easy, and probably overkill for a lot of applications. Even for stuff like boundary conditions for binary search, which could be checked with Hoare logic, I usually handle by stealing the implementation from the Go standard library (so I don't have to think about it). Last year I did advent of code in Lean4. I had written a heap implementation that I didn't end up using. As an exercise, I went back and added proofs for my indicies and a termination proof. I got the termination proof down to `0 < 0` and realized that I had an off by one error (I'd used the math for a 1-based array with a 0-based array). My take-away was that this stuff can catch real bugs, but also that people are not going to do this stuff day-to-day. Maybe some equality saturation thing will make it possible for the compiler to sort out the proof in most cases. If the compiler can hit 80%, you could use it as a linter. (If you want something stricter, you can do totality checking but have escape hatches like Idris' assert_total / assert_smaller.) > Even though at the time I wanted xhtml to win the battle of structured formats for the web, in hindsight I now believe messy html 5 was the way to go. The structured vs unstructured thing is also interesting. I came to a similar conclusion years ago. I'd written some heuristics to pull recipes out of web pages, and also use embedded microdata on some pages. I found I got better results with my heuristics because of bad encoding of the structured data. E.g. a web site was missing entire ingredient blocks in their encoding because their process / data model didn't accommodate recipes with multiple ingredient blocks.

deleted 3y ago

[deleted]

PsylentKnight 3y ago

> It is a bit like Esperanto or something like that. Maybe I am just brain damaged from growing up in a world with English and other messy spoken languages but my intuition suggests that perfectly structured languages are possibly the wrong approach. You seem to be implying Esperanto's lack of popularity is related to its regularity, but I don't think it has anything to do with that - it comes down to network effects. It's not an official language in any country. There are very, very few native speakers of Esperanto. Of those blessed few, they obviously have at least one other native language, otherwise they'd be completely cut off from society. And by the same token, English is popular as a second language due to network effects and the benefits learning it can confer (read: better economic opportunities) and little to do with its regularity. A lot of people have had the experience of learning a bit of Spanish and realizing that English's spelling system is atrociously irregular and we gain nothing by having so many spelling rules that have so many exceptions they can hardly be considered "rules". In fact, English's spelling used to be much more regular, it's just that our pronunciations have shifted a lot over time while the spelling has remained relatively static. This is all tangential to your larger point, I just like talking about this kind of thing.

thr_ddv 3y ago

>The compiler still cannot tell when our loops will terminate (yes, this is possible). while(n < busy_bever(10)) n++ Tell me when my loop terminates.

littlestymaar 3y ago
That's not a very good exemple because with BB we know the code terminates, by definition. The canonical tong-in-cheek argument is to use the Collatz conjoncture instead (but even that isn't a good example in practice: https://news.ycombinator.com/item?id=21440306 https://news.ycombinator.com/item?id=21440306)
- thr_ddv 3y ago
  I'm not asking if it terminates, I'm asking when it does. After all it's not much use if the number overflows the universe.
  - littlestymaar 3y ago
    But that's not something these kinds of tools are supposed do, even with trivial functions… These tools have no idea about the run-time (and there's no way they coule, since it depends on the load you put on the hardware in parallel of running your program)
    - redjamjar 3y ago
      I agree. There are tools though which are specifically for determining worst-case execution time for e.g. embedded systems which can actually give accurate timing information (upto a point).
  - redjamjar 3y ago
    Yeah, so these tools will not tell you how long it will take to terminate --- only that it will eventually. In the vast majority of cases, that is what you want to know.
  - 3y ago