creata

83 ms·

631.
by creata 5y ago
"Typing is Hard" is a popular list of languages and the decidability of typechecking in them: https://3fx.ch/typing-is-hard.html
632.
by creata 5y ago
> a proof development system, aka dependently typed programming language. There are proof assistants without dependent types, like Isabelle/HOL.
633.
by creata 5y ago
A famous quote in Lee's "Introduction to Smooth Manifolds": > differential geometry is the study of properties that are invariant under change of notation
634.
by creata 5y ago
> If you use any of the popular social media apps (Twitter, TikTok, FB/Instagram, Snapchat), then you can't really claim that you care about your data That's not true. I don't use any of those, and I understand the hu
635.
Little Orphan Impls (2015)(smallcultfollowing.com)
1 points by creata 5y ago|0 comments
636.
by creata 5y ago
For some reason, I always thought that people (well, mostly jwz) were exaggerating when they said that cryptocurrencies contributed to climate change. But 0.1% of global emissions is an insanely large amount for the value that cryptocurre
637.
by creata 5y ago
> implicit calls for the FDA to Do Something and ban the tests Not that you're necessarily wrong, but how did you get that from the article? It didn't seem to me like they wanted a ban.
638.
by creata 5y ago
In a single-winner election, why would you think that? The "minority extremist parties" are going to lose anyway, so why not try to let people vote more honestly, so that they don't need to strategize? For example, I don&#x27
639.
by creata 5y ago
Don't we want voters to be able to just honestly write that they like these small extremist parties? Are you suggesting that we want all the voters to vote for one of the top two parties, out of a fear of wasting their vote?[0] Besid
640.
by creata 5y ago
Off-topic: if you want to post a block of code here, I think your best bet is to indent it with four spaces, instead of using code fences (```).
641.
Primitives for Computational Geometry [pdf](graphics.stanford.edu)
1 points by creata 5y ago|0 comments
642.
by creata 5y ago
Just to be clear, are you suggesting mutual recursion across modules ?
643.
by creata 5y ago
> It's like, why use one synonym and not the other? Sometimes it's because writing things in an immutable manner makes things clearer. That's true in many situations, but in this case the equivalence between the two is so
644.
by creata 5y ago
Tail calls and while loops are essentially equivalent, so why care whether a language prefers one or the other?
645.
RustBelt: Logical Foundations for the Future of Safe Systems Programming (2019)(janestreet.com)
21 points by creata 5y ago|1 comments
646.
by creata 5y ago
> People on HN are trying to cancel Feynman as well. What does the word "cancel" mean to you? Feynman can't be deplatformed since he's dead , and no one can deny his fundamental contributions to physics. > Please
647.
by creata 5y ago
> [philosophy and logic] don't get the same level of hatred that math gets Because children aren't forced to study philosophy and logic for many hours each week. And if you think logicians (even of the non-mathematical variety)
648.
by creata 5y ago
This is a very late response, but thanks, those all seem like great reasons.
649.
by creata 5y ago
> Does anyone have first-hand knowledge of what the mob said on Twitter? The article contains links to a few Twitter posts.[0][1] Keep in mind that they might not be representative. Edit: also consider that your use of the word "mob
650.
by creata 5y ago
Here's what seems to be a follow-up on an MIT webpage: https://orgchart.mit.edu/node/6/letters_to_community/importa... Edit: and for what it's worth, I think many people here are too easily stirred
651.
by creata 5y ago
Okay, it's not insane, it just breaks from a convention followed by practically every programming language (and every logic / engineering / computing course) where integers can be interpreted as booleans. And that might be ok
652.
by creata 5y ago
> the solution for this But what is "this"? I think the only criticism of existing theorem provers at https://practal.com is that Coq uses coercions rather than subtyping. Is there a practical example where Coq just
653.
by creata 5y ago
> Type theorists have coopted much of the landscape of formal / mechanised mathematics, I believe much to its detriment. What foundation would you rather have? And what would it do better / how would it be less "detrimenta
654.
The blue-eyed islanders puzzle(terrytao.wordpress.com)
2 points by creata 5y ago|1 comments
655.
by creata 5y ago
> Currying conflicts with rich "imperative" parameters e.g. overloading, default parameters, keyword parameters. This doesn't contradict anything you said, but I think Idris is a language that curries everything and has de
656.
by creata 5y ago
What's "object-oriented" about that code? I'm suspicious of vague labels like "OOP" and "FP", but even some of the Java docs call Java's streams "functional-style". https://d
657.
by creata 5y ago
> They may just vote "screw you" just for revenge. Sure, but how is that worse than them not turning up at all? > The right to vote includes the right to abstain from voting when one does not care. And you're free to ca
658.
by creata 5y ago
> neither were scalable What do you mean by "scalable"?
659.
by creata 5y ago
You're exaggerating the significance of HoTT. Mathematics is already on a pretty firm foundation. And I somehow doubt Bauer meant any ill intent with that line...[0][1] [0]: https://en.wikipedia.org/wiki/Homotopy_t
660.
by creata 5y ago
> That would require the emission and absorption events location in the space to be the same would it not? I think they're referring to the distance in Minkowski space,[0] where the time component and space component cancel out for

More ›