Viewing profile — ebingdom

Yeah, I only meant as opposed to judgmental equality, not the quality of being a proposition.

> It was to provide a small, parsimonious foundation for all of mathematics with a minimal number of "obvious" commitments, to give us confidence that the mathematics we're doing i…

> I do not understand why homotopy type theory posts are so popular on this website. Martin-Löf type theory (and, therefore, homotopy type theory) is like an idealized programming …

For people who know Rust, Haskell's type classes are like a more general version of Rust's traits. But that comparison suggests the wrong chronology; Haskell's type classes came a …

It's not about biases. Using immutability is not just some personal preference. It's common knowledge that mutability everywhere is a bad practice. That's why there's a trend towar…

> Thankfully, this sort of analysis tends to use "constructive logic"; in which case, we're told why some property isn't provable (either because we're given a counterexample provi…

That's a ridiculously high bar to set before you recognize any progress being made.

> The net effect of this would be that I type "mutable" all over the place You might want to consider adopting a more modern programming style for the benefit of your coworkers (an…

> Reasoning About Software What's wrong with this? I need a way to describe techniques that make it easier to...well I don't even know another way to say it. Maybe I'm biased by my…

I think there might be a loose connection. When you want to prove something using mathematical induction, you must come up with an "induction hypothesis". This requires cleverness …

> It's a bit strange that it got BigInt before Int64 JavaScript has Int64?

> I wish that all language design went through a filter where every character mattered like the designer was in an episode of Squid Game. Yes, I totally support this! Coming from l…

As someone with years of experience writing machine-checked proofs in Coq, I cannot imagine the term "Software Engineer" shifting to that meaning, even though it may make sense whe…

> You might say "but it will make it more confusing for people who already know the FP terms" People who already know FP would be fine. Newcomers would be the ones to suffer. We al…

This is a really uninformed opinion. I'm disappointed that it's currently the top comment. You really think functional programmers don't build composite types?

I agree about the math terminology, but I think it would be more confusing if we created a completely different set of vocabulary for the same concepts. So I don't really know what…

> The lambda calculus is an entirely arbitrary way to organize things in math. It’s not based on nature or truth at all. Lambda calculus, category theory, and logic are essentially…

I wonder why they don't just use the highest precision possible given whatever representation of numbers they're using? I know these extra digits would be unlikely to ever matter i…

Categories are objects and morphisms with identities and composition, subject to some coherence laws characterizing identities and stating the associativity of composition. Categor…

This article is completely incongruous and reveals fundamental misunderstandings of category theory. That's actually being generous; most of the content isn't even coherent enough …

> but does that mean it's a good idea? Yes, to me it does. I love when variables have really tight scopes so I don't need to worry about if/how they are used throughout the rest of…

> Cold start (time to first response, ms) O(100) O(1000) O(10000) Ugh, that's not how big O notation works.

> Welcome to Move, a next generation language for secure, sandboxed, and formally verified programming. I didn't see anything about formal verification in the rest of the documenta…