3 ms·

One random guy tried to formalize OOP on power point. Did he submit for publication? Or is publication on a random thread on HN good enough?

pjmlp 6y ago
I can provide other formalizations, including SIGPLAN papers, but am low on troll food supplies to bother.
- leafboi 6y ago
  Trolling is not allowed here, take your stuff and go to reddit.
  - deleted 6y ago
    [deleted]
  - pjmlp 6y ago
    Speaking at the mirror are we?
    - leafboi 6y ago
      I'm not trolling. I'm serious. You'd be warned if Dang saw that comment. Not even kidding.
      - pjmlp 6y ago
        Well, your answers regarding OO calculus appear to be otherwise. Here is a nice exercise, an FP calculus notation about the semantics of type classes in Haskell. Afterwards, it would be nice to see the lambda calculus for functors in OCaml.
        leafboi 6y ago
        >Well, your answers regarding OO calculus appear to be otherwise. I'm obviously not trolling. You literally admitted you are. I can't flag you, so I'm going to plant a word here that will hopefully attract attention and get some admin to stop you. Stop trolling or fuck off.
        pjmlp 6y ago
        You were the one stating that only FP has a perfect calculus representation, and have dismissed all the posts from everyone that that proved otherwise. I asked for the papers describing specific semantic models of two mainstream FP languages to give you the opportunity to prove your point, instead you threat to flag me, I think Dan will take his own conclusions.
        leafboi 6y ago
        >You were the one stating that only FP has a perfect calculus representation, and have dismissed all the posts from everyone that that proved otherwise. That's my opinion. That's not called trolling. Disagreeing with people respectfully is not called trolling. Saying the shit you said above: that you're out of food to continue trolling me IS trolling. I'd flag you already but you need a certain rep to do that. I'm quite new.. but let's see if Dang actually does his job.
didibus 6y ago
Cardelli wrote a whole book: https://www.worldcat.org/title/theory-of-objects/oclc/34557380 https://www.worldcat.org/title/theory-of-objects/oclc/345573... https://en.m.wikipedia.org/wiki/Luca_Cardelli https://en.m.wikipedia.org/wiki/Luca_Cardelli There's also definitely a lot of published papers about typing OO, like https://ieeexplore.ieee.org/document/316056 https://ieeexplore.ieee.org/document/316056 , https://ieeexplore.ieee.org/document/287603 https://ieeexplore.ieee.org/document/287603 , https://drops.dagstuhl.de/opus/volltexte/2016/6103/ https://drops.dagstuhl.de/opus/volltexte/2016/6103/
- leafboi 6y ago
  https://news.ycombinator.com/item?id=24366735 https://news.ycombinator.com/item?id=24366735
  - didibus 6y ago
    Cardelli is a highly reputed academic. That book is a pretty seminal book, lots of papers refer to it. I'm also not really sure what you're trying to point out. When you talk about a calculi for FP, you're talking about what? Lambda Calculus? If so, the base mathematical model of OOP is the Turing machine. That's the model of computation involved. It's been extensively researched and is absolutely well accepted and recognised by everyone everywhere. Similarly to how there was no mathematical model of Haskell or Idris, etc. There wasn't any for OOP languages either like Java, C++, etc. Any attempt at a mathematical framework over those languages came after, and none of them have a strong one that I know off. Some of them, maybe most especially Idris, did get a lot of inspiration from known typing mathematical models, but still the language itself does not have a full on calculus of itself (correct me if I'm wrong) If you're talking about type theory and type systems as related to provability of computation, that's like a whole other conversation. But even then, there's ton of literature that research type systems that can prove OOP, often focused on subtyping since that's the main typing discipline of most OO languages with static type systems.

pjmlp 6y ago

I can provide other formalizations, including SIGPLAN papers, but am low on troll food supplies to bother.

leafboi 6y ago
Trolling is not allowed here, take your stuff and go to reddit.
- deleted 6y ago
  [deleted]
- pjmlp 6y ago
  Speaking at the mirror are we?
  - leafboi 6y ago
    I'm not trolling. I'm serious. You'd be warned if Dang saw that comment. Not even kidding.
    - pjmlp 6y ago
      Well, your answers regarding OO calculus appear to be otherwise. Here is a nice exercise, an FP calculus notation about the semantics of type classes in Haskell. Afterwards, it would be nice to see the lambda calculus for functors in OCaml.
      - leafboi 6y ago
        >Well, your answers regarding OO calculus appear to be otherwise. I'm obviously not trolling. You literally admitted you are. I can't flag you, so I'm going to plant a word here that will hopefully attract attention and get some admin to stop you. Stop trolling or fuck off.
        pjmlp 6y ago
        You were the one stating that only FP has a perfect calculus representation, and have dismissed all the posts from everyone that that proved otherwise. I asked for the papers describing specific semantic models of two mainstream FP languages to give you the opportunity to prove your point, instead you threat to flag me, I think Dan will take his own conclusions.
        leafboi 6y ago
        >You were the one stating that only FP has a perfect calculus representation, and have dismissed all the posts from everyone that that proved otherwise. That's my opinion. That's not called trolling. Disagreeing with people respectfully is not called trolling. Saying the shit you said above: that you're out of food to continue trolling me IS trolling. I'd flag you already but you need a certain rep to do that. I'm quite new.. but let's see if Dang actually does his job.

didibus 6y ago

Cardelli wrote a whole book: https://www.worldcat.org/title/theory-of-objects/oclc/34557380 https://www.worldcat.org/title/theory-of-objects/oclc/345573... https://en.m.wikipedia.org/wiki/Luca_Cardelli https://en.m.wikipedia.org/wiki/Luca_Cardelli There's also definitely a lot of published papers about typing OO, like https://ieeexplore.ieee.org/document/316056 https://ieeexplore.ieee.org/document/316056 , https://ieeexplore.ieee.org/document/287603 https://ieeexplore.ieee.org/document/287603 , https://drops.dagstuhl.de/opus/volltexte/2016/6103/ https://drops.dagstuhl.de/opus/volltexte/2016/6103/

leafboi 6y ago
https://news.ycombinator.com/item?id=24366735 https://news.ycombinator.com/item?id=24366735
- didibus 6y ago
  Cardelli is a highly reputed academic. That book is a pretty seminal book, lots of papers refer to it. I'm also not really sure what you're trying to point out. When you talk about a calculi for FP, you're talking about what? Lambda Calculus? If so, the base mathematical model of OOP is the Turing machine. That's the model of computation involved. It's been extensively researched and is absolutely well accepted and recognised by everyone everywhere. Similarly to how there was no mathematical model of Haskell or Idris, etc. There wasn't any for OOP languages either like Java, C++, etc. Any attempt at a mathematical framework over those languages came after, and none of them have a strong one that I know off. Some of them, maybe most especially Idris, did get a lot of inspiration from known typing mathematical models, but still the language itself does not have a full on calculus of itself (correct me if I'm wrong) If you're talking about type theory and type systems as related to provability of computation, that's like a whole other conversation. But even then, there's ton of literature that research type systems that can prove OOP, often focused on subtyping since that's the main typing discipline of most OO languages with static type systems.