remexre

53 ms·

1. 601.▲
   by remexre 6y ago

   I think Cubical Type Theory (derived from HoTT) is a part of the future for general-purpose dependently-typed programming -- it has canonicity, which I'd argue is necessary for a general-purpose programming language, and it being suita
2. 602.▲
   by remexre 6y ago

   Is this an old draft of the book? http://saunders.phil.cmu.edu/book/hott-online.pdf EDIT: Should've read the first page, whoops; still, the book provides a lot more material, so if you're interested, give it
3. 603.▲
   by remexre 6y ago

   Torrent clients are legal though? And prosecution has generally followed the "if a tool isn't advertising 'you can use this to circumvent the law,' it's the user that's liable for an illegal use, not the develo
4. 604.▲
   by remexre 6y ago

   I'm kinda annoyed this is the case before the GBM/EGLStreams argument got resolved... I've done some programming against GBM directly (wanted an OpenGL ES application to be in a "kiosk mode," didn't want to hav
5. 605.▲
   by remexre 6y ago

   I use DDG despite needing to search Google often, because the bang commands (!w, !wa, !hackage, !g) are so dang nice to have.
6. 606.▲
   by remexre 6y ago

   Oh, this programming model (and overall goal) look quite like http://witheve.com/
7. 607.▲
   by remexre 6y ago

   Is there a paper about how their computing paradigm works? Basically the only thing I got from that page was, "damn, I'm glad I don't need to use gluesticks when I code."
8. 608.▲
   by remexre 6y ago

   DTRT = do the right thing idk the others
9. 609.▲
   by remexre 6y ago

   > Go ask a Haskell developer and the first reaction you will get is probably "wait, you were running getData inside the original function?!" Haskell developer here, this was indeed my first reaction :P
10. 610.▲
    by remexre 6y ago

    IIRC, the match it generates often ends up being a dependent match using the convoy pattern once nontrivial functions start being written, which quickly gets really really hard to read. Maybe this is partly the fault of Coq's matching
11. 611.▲
    by remexre 6y ago

    Whitespace was created by Edwin Brady, notably the same creator of the much more practical Idris language: https://www.idris-lang.org/
12. 612.▲
    by remexre 6y ago

    > I don't understand what this is supposed to mean. How are e.g. coq tactics not the exact same? Well, I've never gotten `induction' to generate anything close to a readable program -- hopefully this is better?
13. 613.▲
    by remexre 6y ago

    Right, I think the point is that you no longer have atomic semantics for the write as a whole.
14. 614.▲
    by remexre 6y ago

    I'm kinda surprised none of the model-checking people have tried verifying glibc's NPTL implementation; I guess it might be hard to formalize futex's behavior?
15. 615.▲
    by remexre 6y ago

    I think you'd want a differentiable language to make that easy.
16. 616.▲
    by remexre 6y ago

    This looks quite like https://rr-project.org/ -- I wonder if it scales as well.
17. 617.▲
    by remexre 6y ago

    To be fair, the majority (vast majority?) of people who get paid to work on the kernel do in fact have to endure HR bullshit, salary negotiations, etc.; they're just doing it with Intel HR or Qualcomm HR rather than Linux Foundation HR
18. 618.▲
    by remexre 6y ago

    The complaint is about the translation, not the term.
19. 619.▲
    by remexre 6y ago

    This feels like it's getting just up to the point of saying "thus, monads"...
20. 620.▲
    by remexre 6y ago

    Same, but I think that's an argument for making your social space the opposite
21. 621.▲
    by remexre 6y ago

    Most Lisp libraries won't automatically work with Parenscript -- think of Parenscript as just being more Lisp-like syntax for JS, rather than a compile from Lisp to JS. It's quite useful if you want to dynamically generate JS, or
22. 622.▲
    by remexre 6y ago

    Huh, a friend of mine was complaining that you couldn't do something similar -- advertise services with their port numbers via DNS, so you could e.g. host a dozen Minecraft servers from a single IP (with a dozen different hostnames poi
23. 623.▲
    by remexre 6y ago

    Had to track down a friend with a Mac, but Mumble appears to have an RNNoise option there.
24. 624.▲
    by remexre 6y ago

    I'm actually playing with a message-passing-based UI system right now, mostly as a prototype; long story below. I'm making it considerably more Erlangy than yours -- essentially, you have message-passing with a sequential/dir
25. 625.▲
    by remexre 6y ago

    I haven't used a Mac in ages, so I'm unfamiliar with any unique features of Cocoa over what one gets with e.g. GTK+; what would you say the features that make it better are? I'm usually a bit skeptical of current-generation G
26. 626.▲
    by remexre 6y ago

    Are the correct semantics instead (llvm.maximum undef, %x) -> %x ? NaNs are one of the bigger parts of IEEE754 that make me wish posits could take over...
27. 627.▲
    by remexre 6y ago

    I think a large part of this is that Denmark has an expansive social welfare system, which they're quite proud of. Given that reductions in carbon emissions are claimed by some prominent voices to be expensive, economy-tanking things,
28. 628.▲
    by remexre 6y ago

    There's also the open-source RNNoise -- I know Mumble added support for it recently, and it's _amazing_ -- if we were allowed to use it for work, I'd prefer it for voice-only stuff over Zoom.
29. 629.▲
    by remexre 6y ago

    I want Linux from a trusted source, so I compile it myself :P If you can get the kernel building (that repo), you can use any distro; that repo even has packages bundled for Debian, Arch, and Fedora.
30. 630.▲
    by remexre 6y ago

    Arc "feels" a lot more Scheme-like than Common Lisp-like, but pg is a CL guy afaik; my observations on the two: Scheme avoids type errors by writing programs which could be given static types with a sufficiently powerful type-chec