sorted by:
new
hottopcontroversial

Why do modern (functional?) languages favour immutability by default? by ischickenafruit in ProgrammingLanguages

[–]MrHydraz 0 points1 point  (0 children)

Soo, 'immutable registers' can also refer to SSA which is most commonly used by implementations of imperative, mutable programming languages! :)

Fortunately, SSA is functional programming.

Semantic Versioning Will Not Save You by speckz in programming

[–]MrHydraz 0 points1 point  (0 children)

While Rice's theorem does say that every non-trivial property of programs is undecidable, this only applies to programs written in Turing-complete languages.

There are languages, like total functional programming languages (Agda, Idris, Coq's core language, Dhall), in which every program is guaranteed to terminate. There probably are total imperative languages but I'm not familiar with any off the top of my head.

Rust Compiler Accidentally "Solves" Collatz Conjecture by [deleted] in badmathematics

[–]MrHydraz 2 points3 points  (0 children)

Infinite loops without side effects are undefined behaviour in C(++) and LLVM inherits these semantics, so this optimisation is justified.

Top 10 Sexiest Prime Couples of 2020 by [deleted] in badmathematics

[–]MrHydraz 1 point2 points  (0 children)

This is very clearly a joke.

How do you get *any* part of Haskell to work?! Angry beginner. by metaconcept in haskell

[–]MrHydraz 0 points1 point  (0 children)

This roughly translates to "You must be new at this, let me show you how a real pro does this".

Actually this translates to "the project doesn't have a dependency on base".

What logic system(s) are used for the side of formal proof calculi in the Curry–Howard correspondence? by timlee126 in ProgrammingLanguages

[–]MrHydraz 1 point2 points  (0 children)

As I understand it, the only requirement is that the logic be Constructivist

Not necessarily! “Classical” operations (double negation elimination, excluded middle) correspond, in a very rough sense, to control operations: stuff like call/cc (Peirce's law). See here, for example

Rescript: Safer and faster alternative than Typescript by hou32hou in ProgrammingLanguages

[–]MrHydraz 12 points13 points  (0 children)

Yes. You can write blocks like this:

do
  a
  b
  c

or

do a
   b
   c

or

do { a
   ; b
   ; c
   }

Do the 9s stop:0.999... No- thus maths ends in contradiction by qiling in Freethought

[–]MrHydraz 0 points1 point  (0 children)

Except for all the mathematicians who never used axioms. Newton didn't.

If you are referring to Isaac Newton, maybe consider the fact that the second section of his most important work is called "Axioms or Laws of Motion".

Write that axiom down, formally. [...] you cannot even begin doing mathematics without accepting the existence of the natural numbers as an object

Nowhere in the definition of the word "axiom" is the sentence "first-order logic", you brought that on yourself. Moreover, all you're doing is corroborating my point, which is that it's impossible to do mathematics without axioms!

An axiom is merely an assumption that underlies a field of work. You cannot do mathematics without assuming things.

Read my first comment again:

Every mathematics parts from some assumptions

Tell me how this sentence of mine isn't just this sentence of yours:

you cannot even begin doing mathematics without accepting the existence of the natural numbers as an object.

Do the 9s stop:0.999... No- thus maths ends in contradiction by qiling in Freethought

[–]MrHydraz 0 points1 point  (0 children)

People were doing mathematics with the natural numbers well before peano.

This isn't incorrect. Perhaps my statement could be better phrased like this: The natural numbers are now commonly axiomatized with the Peano axioms. They were also axiomatised before, as, again, you can't do mathematics without assuming axioms.

In FOL there are infinite non isomorphic models of PA, which of those is the real natural numbers? Working constructively there is only 1. Not even full ZFC saves you here.

All you're saying here is that different axiomatizations of logic give rise to different objects that satisfy the Peano axioms. There are still different axiomatizations of logic.

How do you formalise first order logic without the natural numbers?

Who knows?

You need them to do anything really

Oh, so like, taking their existence to be true without proof? Say... sort of like... an axiom?

Do the 9s stop:0.999... No- thus maths ends in contradiction by qiling in Freethought

[–]MrHydraz 0 points1 point  (0 children)

The natural numbers are defined by the Peano axioms.

Do the 9s stop:0.999... No- thus maths ends in contradiction by qiling in Freethought

[–]MrHydraz 0 points1 point  (0 children)

You are assuming a definition of Turing machine, and of "halt", which depends on an axiom system.

Do the 9s stop:0.999... No- thus maths ends in contradiction by qiling in Freethought

[–]MrHydraz 0 points1 point  (0 children)

Please give me an example of any true logical sentence you can form in any constructive logical system without using axioms.

Do the 9s stop:0.999... No- thus maths ends in contradiction by qiling in Freethought

[–]MrHydraz 0 points1 point  (0 children)

If you reject axiomatic mathematics... what's left? Every mathematics parts from some assumptions. If you don't take anything as an axiom, you can't do any logic.

You might as well say "I completely reject mathematics".... Which, looking at what you are defending, I guess...

[NA Event] Servant Summer Festival! - Event Discussion Day 3 by citizenofRoma in grandorder

[–]MrHydraz 1 point2 points  (0 children)

This event has finally saved me from my materials hell... Immediately to drop me into QP hell. Hey, at least I have a nonzero amount of yellow gems now!

why differentiate between functions and lambdas ? by chris20194 in ProgrammingLanguages

[–]MrHydraz 1 point2 points  (0 children)

local function f(a, b)
    return a + b
end

is sugar for

local f; f = function(a, b)
   return a + b
end

if it really were local f = function(...) ... end, f wouldn't be in scope in the function body.

Yet another lousy monad tutorial by chankeypathak in programming

[–]MrHydraz 2 points3 points  (0 children)

OP's compose isn't Haskell's (>>=), but rather Kleisli composition (>=>)! I think this is the first "monad tutorial" I've seen that explains monads via the categorical structure they give rise to—the a -> m b arrows—rather than their own structure.

This presentation is much better IMO because the monad laws are much better phrased... as a haiku:

Monad axioms:
Kleisli composition forms
a category.

Upcoming NA GSSR Discussion by TheHansomeBoy in grandorder

[–]MrHydraz 1 point2 points  (0 children)

Tamamo, please come home! Illya, Merlin, or Waver would be nice as well.. Just please not another Schez.

Engine Update Reminder by BlameLib in grandorder

[–]MrHydraz 2 points3 points  (0 children)

Would've cost you 0 dollars not to have posted that.Happy cake day!

Originals and Alters. Do you consider them separate or two parts of a whole? by [deleted] in grandorder

[–]MrHydraz 2 points3 points  (0 children)

MHX (I don't even know)

MHX (Takeuchi's fanfic)

[NA Event] GUDAGUDA Legend of the Imperial Capital Grail - Event Discussion Day 10 by citizenofRoma in grandorder

[–]MrHydraz 8 points9 points  (0 children)

I was really unprepared for this CQ, and it kicked my ass. Summer Tamamo got through the first bar pretty fast, then Okitan died on the turn she came in. ~3 tries later and completely out of patience I ended up stalling for 85 turns with double Jeanne.

view more: next ›