waluigi's comments

It’s even more counterintuitive than you let on! If you are working in ZFC along with the axiom “ZFC is consistent” then there’s no issue: just a normal number[1]. Where things get really strange is in ZFC plus the axiom “ZFC is inconsistent”.

This already sounds like an inconsistent theory, but surprisingly isn’t: Godel’s second incompleteness theorem directly gives us that Con(ZFC) is independent, so there are models that validate both Con(ZFC) and ~Con(ZFC). The models that validate ~Con(ZFC) are very confused about what numbers are: from the models perspective, there is a number corresponding to a Godel code for the supposed proof of inconsistency, but from the external view this is a “nonstandard number”: it’s not not a finite numeral!

Getting back to BB(748): what does this look like in a model of ZFC + ~Con(ZFC)? We can prove that the machine internal to the model will find that astronomically large Godel code, so BB(748) will be a nonstandard number. In other words, you can tell if a 748 state machine will terminate in this model: you’ve just got to run it for a number of steps that’s larger than every finite numeral!

[1]: unless there’s some machine that with 748 that enumerates theorems of ZFC+Con(ZFC) but that’s a different discussion.

Defining x/0 as 0 doesn’t break anything mathematically; all the relevant field axioms have an x != 0 hypothesis so this really is undefined behavior.

Moreover, it’s actually pretty common for proof assistants to adopt the x/0 = 0 convention, as it turns a partial function into a total one! Having something like NaN or Inf is definitely a better solution in practice, but x/0 = 0 does have its merits!

I think what the poster above is saying is that by saying "the pentagon" the author is referring to the (unique) 5 sided regular polygon, as opposed to some random, potentially non-regular 5 sided polygon.

I would push back against this. There is definitely a pretty steep learning curve, but once you are over it you really start to reap the benefits of being able to rapidly add niche functionality that exactly fits your workflows.

The way I would approach this is to write what essentially amounts to a declarative specification of what computation needs to be run, and then define an interpreter that handles the caching of intermediate values.

The "Embedded DSL + Interpreter" pattern is incredibly powerful, and it's nice to see it catching on more.

Monad Transformers aren't _that_ bad, the MTL style of doing things makes it all pretty painless.

It also provides a huge opportunity for testing. At a very high level, you describe all of your effects as a series of embedded, compostable DSLs that you define interpreters for. The awesome part is that you can switch out the interpreters at will, so you can, for example, replace something that handles network requests with something that returns dummy data almost effortlessly.

F#'s object model is very different from OCaml's. F# is basically the same as C# when it comes to objects, but OCaml has some sense of structural subtyping that F# lacks. On top of that, OCaml has a very powerful module system, whereas F# has a pretty standard one.

On the other hand, F# has computation expressions (essentially extensible syntax sugar for certain kinds of operations), as well some nice extensions to the pattern match system.

That's not to say one is exactly better than the other, they just focus on doing different things.

This owns. It's important to realize that a lot of at-risk populations that would most benefit from medication are often the most economically disadvantaged, and that our current healthcare system often excludes them from the help they need. Obviously, lab-grade medication is less risky than stuff that's been produced in a mason jar, but when the choice is between having access to life-saving medical equipment or not, the choice is pretty clear. If you have concerns with how this could hurt people, then the best solution would be to make sure that everyone has access to the care they need, rather then allocating care on the basis of how much they can afford.

Thank you for pointing this out. It seems that "Governments are ineffective" is taken as a universal truth around here, without considering the fact that pro-privatisation governments have a very strong incentive to make programs inefficient. If you want a more efficient government, vote for people who support government programs.

Its a common misconception that proofs by contradiction are not constructive. Take the proof that √2 is irrational. What you are trying to prove is that √2 is not rational, or, constructively speaking, `√2 ∈ ℚ => ⊥`. So a proof that constructs such a function must construct a contradiction given the fact that √2 is irrational. This is both a proof by contradiction and a constructive proof. The same can be done with both of the proof you mentioned. Where you really start to run in to trouble is double negation. Evidence of ~~P comes as some function `(P -> ⊥) -> ⊥`, so there isn't really any way to create evidence of P from that. The lack of LEM really stems from this fact. If you try to run through the proof that `P v ~P => T`, you get stuck on double negation. However, it is true that `~~(P v ~P) => T`, which satisfies the gut feeling that LEM can't _not_ be true.

Yeah, effect systems in general are a really cool idea that I wish we saw more of. Haskell and its derivatives are the only semi popular languages that have some sort of system, and those are just a few points in the design space that admittedly aren't perfect.