3 ms·

> Thus the computer is in fact a tool designed to facilitate this logic game. The computer is in itself a simulator of a simple game involving formal rules with

> Thus the computer is in fact a tool designed to facilitate this logic game. The computer is in itself a simulator of a simple game involving formal rules with assembly language terms as the axioms. It's somewhat poetic, beautiful and accidentally funny that your argument frays at the same blind spots that your tone does, which is at the gap between theoretical and on-the-ground meaning. It is true in a theoretical sense that you could describe a computer as a simulator which can be modeled with formal rules. But it tells me nothing about why the computer as a mass-market electronic device which runs mass-market software occupies the societal role it does, nor where it will go, nor why it was an innovation which transformationally altered society in the same way as the flame, the wheel, the chariot, the bow, the written word, the loom, the printing press. Now, if you're not going to try and engage with any of that because "It probably can be done, I just can't spare the effort" what do you think is more likely: 1) your complaint most loudly voices new and fresh insight to the industry which it had previously missed 2) your complaint most loudly voices your own gaps in curiosity and understanding If it's 2, then I just think that's sad. I see a lot of engineers (frequently early-stage in their careers and suffering from a bit of imposter syndrome) get stuck in a rut where they dogmatically devour formalism as a vehicle to elevate the level and quality of their engineering to the level of rigor seen in the sciences. But the appropriation of surface level aesthetics masks a methodological inability to do the dirty work to get the actual job done via "less sexy" paths (as reality often requires), to differentiate and harden critical sections when necessary. It's sad because it generally only speaks to their own lack of exposure with just how power and impact software can be built to have, and it takes the momentary weakness of inexperience and calcifies it into eternal inexperience and terminal juniority owing to an unrealistic, radioactive hubris far out of proportion with actual capability. That could be you. It doesn't have to be.

Geminidog 6y ago
> It is true in a theoretical sense that you could describe a computer as a simulator which can be modeled with formal rules. "Could be described this way"? The entire theory of computer science is built off of this premise. The theory of computing was derived in a logical game of axioms and theorems before a physical computer was actually invented. I don't think you're very familiar with this topic. >But it tells me nothing about why the computer as a mass-market electronic device which runs mass-market software occupies the societal role it does, nor where it will go, nor why it was an innovation which transformationally altered society in the same way as the flame, the wheel, the chariot, the bow, the written word, the loom, the printing press. So what does this have to do with anything? We're talking about the formalization of software module organization everything you're talking about is going off topic. Society, the wheel the chariot have nothing to do with the main point. >Now, if you're not going to try and engage with any of that because "It probably can be done, I just can't spare the effort" what do you think is more likely: I'm not playing games with you. I honestly think that my point on how the software industry loves to repeat history with their design philosophies is pretty obvious and well known. Your asking for a proof which I'm simply going to say I have none, look it up yourself, I don't want to create a bibliography for a point I find obvious. The length of my responses should tell you that I'm giving you a lot of my attention and I'm not just opening an escape hatch here. >1) your complaint most loudly voices new and fresh insight to the industry which it had previously missed. Missed by industry. Not missed by academia. There are much is 100x more research in this area in academia that is largely ignored by industry. I don't blame the industry. No real miracles coming out of academia yet, but the approach is correct. There research does indeed come closer and closer to our intuitive notions of what is good design and what is a correct program. >2) your complaint most loudly voices your own gaps in curiosity and understanding So? Then tell me how my gap in understanding is reflected in my POINT rather then in my character. consider a third possibility. 3) My complaint is neutral and simply stating a minor point but the other party wants to turn it into an exploration of the my personality. Possibly because he desires to win in the argument and sees no avenue to win through logic and thus turns to more crude methodologies like declaring the other party as having "gaps in knowledge" and declaring him as "sad" If there is a gap in knowledge point it out exactly, don't speculate at the probability of it's existence. Look man, argue your point and my point. My character is irrelevant. If you deviate and start talking about my personal character it's just a sign that you've run out of any logical merits to stand your ground. I'm helping you right now. Lay off the insults and discuss my points only. Don't go meta and talk about how I could be wrong or lack knowledge. Talk about how the point is wrong and that helps your argument. >If it's 2, then I just think that's sad. Look dude. That right there is grounds for a flag. That's my last warning. Argue my point and don't get personal. >get stuck in a phase where they dogmatically devour formalism as a vehicle to elevate the level and quality of their engineering to the level of rigor seen in the sciences. I've never seen this phase ever. Nobody does it in industry because such formalism on software module design aren't fully fleshed out to my knowledge. The closest you'd get in industry is Haskell and even then much of it is still design. >But the appropriation of surface level aesthetics masks a methodological inability to arrive at the reality via "less sexy" paths (as reality often requires), to differentiate and harden critical sections when necessary. You mean arrive at solutions without formalism which is done all the time and easily by anyone? Formalism is 100x harder then the status quo and it's incomplete. It's not done in industry at all because it basically can't be done as the tooling isn't available. Have you ever seen Idris in production? I haven't. What is your point. >It's sad because it generally only speaks to their own lack of exposure with just how robustly software can be built, Like 99.9999% of all software is built informally. That's all the exposure you can get. It's 100x more rare to get formal verification outside of academia. I literally don't know what you're talking about here. The only automated "formalism" in the industry is type checking and that's as far as it goes. Plenty of software that's pretty stable is built this way. See windows and linux. Obviously the methodology to make these pieces of software relatively bug free and well designed is done through artificial selection. Endless iterations of refactoring code and fixing bugs until the software gets closer to perfection to a software engineers intuitive sense of perfection. This method can be done and is done all the time... Again, what is your point? >That could be you. It doesn't have to be. So what? Who cares if it's me? How does this matter to you and what does this have to do with the topic? I want you re-visualize the situation here. Pretend I don't exist and the only thing that exists is the topic and your task is to prove it wrong. Literally that's the only reason why I'm here. If you got something to say that's on topic, say it and I can learn from it or I can make you learn from your error. That's it. Talking about some vague probabilities on how I'm more likely to be wrong when compared to the industry isn't going to go anywhere. Additionally the industry isn't exactly the smartest thing in the world. The industry invented JavaScript and now they use typescript to hide their mistake.
- yowlingcat 6y ago
  > So? Then tell me how my gap in understanding is reflected in my POINT rather then in my character. Not only have I already done so, so too have a bunch of other accounts. Why don't you re-read what they've all said and think about it some more? I'm sure you'll be able to find something more useful to add if you do that. > So what? Who cares if it's me? How does this matter to you and what does this have to do with the topic? Because if you do that, you will never fully mature as an adult human being. You'll repel others away from you and then feel the pain of isolation and loneliness. You'll watch others live rich lives you wish you had. I think that is a very unfortunate path. I hope you will avoid that pain for yourself before it's too late and you can't redo all the time you will inevitably kick yourself for wasting. Life goes by very quickly and you don't get chances for do-overs.
  - Geminidog 6y ago
    This is obviously a troll. We're done here.
    - pcen 6y ago
      Thank you for putting in the good fight. It will take a high-profile level catastrophe akin to the Challenger Disaster for the industry to move on from the current state and formalize even basic things we've known for decades such as category theory and functional programming. And unfortunately, the results will be heavy regulation. Until then, we will just have to watch history repeat through these types of discussions. [0] [0] https://github.com/promises-aplus/promises-spec/issues/94 https://github.com/promises-aplus/promises-spec/issues/94
      - deleted 6y ago
        [deleted]
      - Geminidog 6y ago
        Please don't continue this thread. Whether you agree with me or not, it has devolved into personal and character insults by the other poster. You can continue the discussion with me somewhere else in the thread just not under yowlingcat. Blood has been spilled (figuratively) and tensions are extremely high. Suffice to say, I'm not talking directly about category theory, that's one possibility of formalization (that seems quite unlikely). Other parts that have successfully made it into programming (and have changed programming for the better) including complexity theory, type theory and the Rust borrow checker. Two theories automate correctness and one is helpful in analysis of execution speed. My proposal is about one for modular organization and while category theory is a great candidate, it does have an incredibly high learning curve and to me that is why I agree with you that it is an unlikely candidate. I mean it does sort of exist already as a type checker in haskell... I'm more saying that I don't expect people to actually try to learn CT. Either way, I believe more formality can be done and we don't have to force the entire industry to use monads and FP (FYI I prefer the style myself). If a formal theory about modular organization ever comes into vogue my guess is that it will exist more popularly as a "design pattern" in the industry rather than a programming framework or formal method. People can choose to use a pattern, or bend the rules... the main point and the crux of my entire effort is to say something along the lines of the fact that we need design patterns that provably improves "design." Without proof most of our efforts seem like steps to the side rather than forward. If you have a reply, please place it directly under my parent post, not here. edit: That github link is picture perfect mirror of what I'm talking about in the industry. Thumbs up for bringing it to my attention.

Geminidog 6y ago

> It is true in a theoretical sense that you could describe a computer as a simulator which can be modeled with formal rules. "Could be described this way"? The entire theory of computer science is built off of this premise. The theory of computing was derived in a logical game of axioms and theorems before a physical computer was actually invented. I don't think you're very familiar with this topic. >But it tells me nothing about why the computer as a mass-market electronic device which runs mass-market software occupies the societal role it does, nor where it will go, nor why it was an innovation which transformationally altered society in the same way as the flame, the wheel, the chariot, the bow, the written word, the loom, the printing press. So what does this have to do with anything? We're talking about the formalization of software module organization everything you're talking about is going off topic. Society, the wheel the chariot have nothing to do with the main point. >Now, if you're not going to try and engage with any of that because "It probably can be done, I just can't spare the effort" what do you think is more likely: I'm not playing games with you. I honestly think that my point on how the software industry loves to repeat history with their design philosophies is pretty obvious and well known. Your asking for a proof which I'm simply going to say I have none, look it up yourself, I don't want to create a bibliography for a point I find obvious. The length of my responses should tell you that I'm giving you a lot of my attention and I'm not just opening an escape hatch here. >1) your complaint most loudly voices new and fresh insight to the industry which it had previously missed. Missed by industry. Not missed by academia. There are much is 100x more research in this area in academia that is largely ignored by industry. I don't blame the industry. No real miracles coming out of academia yet, but the approach is correct. There research does indeed come closer and closer to our intuitive notions of what is good design and what is a correct program. >2) your complaint most loudly voices your own gaps in curiosity and understanding So? Then tell me how my gap in understanding is reflected in my POINT rather then in my character. consider a third possibility. 3) My complaint is neutral and simply stating a minor point but the other party wants to turn it into an exploration of the my personality. Possibly because he desires to win in the argument and sees no avenue to win through logic and thus turns to more crude methodologies like declaring the other party as having "gaps in knowledge" and declaring him as "sad" If there is a gap in knowledge point it out exactly, don't speculate at the probability of it's existence. Look man, argue your point and my point. My character is irrelevant. If you deviate and start talking about my personal character it's just a sign that you've run out of any logical merits to stand your ground. I'm helping you right now. Lay off the insults and discuss my points only. Don't go meta and talk about how I could be wrong or lack knowledge. Talk about how the point is wrong and that helps your argument. >If it's 2, then I just think that's sad. Look dude. That right there is grounds for a flag. That's my last warning. Argue my point and don't get personal. >get stuck in a phase where they dogmatically devour formalism as a vehicle to elevate the level and quality of their engineering to the level of rigor seen in the sciences. I've never seen this phase ever. Nobody does it in industry because such formalism on software module design aren't fully fleshed out to my knowledge. The closest you'd get in industry is Haskell and even then much of it is still design. >But the appropriation of surface level aesthetics masks a methodological inability to arrive at the reality via "less sexy" paths (as reality often requires), to differentiate and harden critical sections when necessary. You mean arrive at solutions without formalism which is done all the time and easily by anyone? Formalism is 100x harder then the status quo and it's incomplete. It's not done in industry at all because it basically can't be done as the tooling isn't available. Have you ever seen Idris in production? I haven't. What is your point. >It's sad because it generally only speaks to their own lack of exposure with just how robustly software can be built, Like 99.9999% of all software is built informally. That's all the exposure you can get. It's 100x more rare to get formal verification outside of academia. I literally don't know what you're talking about here. The only automated "formalism" in the industry is type checking and that's as far as it goes. Plenty of software that's pretty stable is built this way. See windows and linux. Obviously the methodology to make these pieces of software relatively bug free and well designed is done through artificial selection. Endless iterations of refactoring code and fixing bugs until the software gets closer to perfection to a software engineers intuitive sense of perfection. This method can be done and is done all the time... Again, what is your point? >That could be you. It doesn't have to be. So what? Who cares if it's me? How does this matter to you and what does this have to do with the topic? I want you re-visualize the situation here. Pretend I don't exist and the only thing that exists is the topic and your task is to prove it wrong. Literally that's the only reason why I'm here. If you got something to say that's on topic, say it and I can learn from it or I can make you learn from your error. That's it. Talking about some vague probabilities on how I'm more likely to be wrong when compared to the industry isn't going to go anywhere. Additionally the industry isn't exactly the smartest thing in the world. The industry invented JavaScript and now they use typescript to hide their mistake.

yowlingcat 6y ago
> So? Then tell me how my gap in understanding is reflected in my POINT rather then in my character. Not only have I already done so, so too have a bunch of other accounts. Why don't you re-read what they've all said and think about it some more? I'm sure you'll be able to find something more useful to add if you do that. > So what? Who cares if it's me? How does this matter to you and what does this have to do with the topic? Because if you do that, you will never fully mature as an adult human being. You'll repel others away from you and then feel the pain of isolation and loneliness. You'll watch others live rich lives you wish you had. I think that is a very unfortunate path. I hope you will avoid that pain for yourself before it's too late and you can't redo all the time you will inevitably kick yourself for wasting. Life goes by very quickly and you don't get chances for do-overs.
- Geminidog 6y ago
  This is obviously a troll. We're done here.
  - pcen 6y ago
    Thank you for putting in the good fight. It will take a high-profile level catastrophe akin to the Challenger Disaster for the industry to move on from the current state and formalize even basic things we've known for decades such as category theory and functional programming. And unfortunately, the results will be heavy regulation. Until then, we will just have to watch history repeat through these types of discussions. [0] [0] https://github.com/promises-aplus/promises-spec/issues/94 https://github.com/promises-aplus/promises-spec/issues/94
    - deleted 6y ago
      [deleted]
    - Geminidog 6y ago
      Please don't continue this thread. Whether you agree with me or not, it has devolved into personal and character insults by the other poster. You can continue the discussion with me somewhere else in the thread just not under yowlingcat. Blood has been spilled (figuratively) and tensions are extremely high. Suffice to say, I'm not talking directly about category theory, that's one possibility of formalization (that seems quite unlikely). Other parts that have successfully made it into programming (and have changed programming for the better) including complexity theory, type theory and the Rust borrow checker. Two theories automate correctness and one is helpful in analysis of execution speed. My proposal is about one for modular organization and while category theory is a great candidate, it does have an incredibly high learning curve and to me that is why I agree with you that it is an unlikely candidate. I mean it does sort of exist already as a type checker in haskell... I'm more saying that I don't expect people to actually try to learn CT. Either way, I believe more formality can be done and we don't have to force the entire industry to use monads and FP (FYI I prefer the style myself). If a formal theory about modular organization ever comes into vogue my guess is that it will exist more popularly as a "design pattern" in the industry rather than a programming framework or formal method. People can choose to use a pattern, or bend the rules... the main point and the crux of my entire effort is to say something along the lines of the fact that we need design patterns that provably improves "design." Without proof most of our efforts seem like steps to the side rather than forward. If you have a reply, please place it directly under my parent post, not here. edit: That github link is picture perfect mirror of what I'm talking about in the industry. Thumbs up for bringing it to my attention.