Tainnor

42 ms·

691.
by Tainnor 2y ago
In my opinion, exceptions should be for really exceptional situations - things you can't realistically expect and/or which just signal a programming error (e.g. a precondition being violated). They aren't usually recoverable
692.
by Tainnor 2y ago
There's nothing morally wrong with it, it's just not an environment where I'm likely to be comfortable.
693.
by Tainnor 2y ago
"Soft" limits as guidelines are fine (although in my experience they are often completely unrealistic - e.g. set up a spring boot app with tests, CI config and kubernetes deployment, that implements API XY - all in 4h). But a hard
694.
by Tainnor 2y ago
All of these have happened to me: - The interviewer is wearing a suit. - The interviewer asks "you've worked with [person who now works at our company] before, what do you think about them?". Bonus points if they insist after
695.
by Tainnor 2y ago
You can't define a model "NPA" in which all numbers are nonpositive but then define multiplication such that it can yield positive numbers - that just wouldn't be a function. It's pretty easy to prove that S(0)*S(0)
696.
by Tainnor 2y ago
I'm personally not a constructivist or even finitist (mostly for pragmatic reasons), but discussions about Gödel get sidetracked by musings about either of these philosophies so often that I feel it's important to point out that t
697.
by Tainnor 2y ago
> Similarly, it seemed to David Hilbert like it should be possible to have a system of formal logic that all could accept, which would prove itself to be consistent. Minor nitpick, but I don't think this fully captures the essence o
698.
by Tainnor 2y ago
> In the case of the complex numbers, if you just exchange i and -i, I believe that you get a field which is fully isomorphic to C. To add to this and expand a little, there are only two isomorphisms between C and itself which keep all t
699.
by Tainnor 2y ago
In every model of a theory, you can just consistently relabel elements in order to get another model. But that doesn't really tell you anything because that model is just isomorphic to the old one (that term has a precise meaning, but
700.
by Tainnor 2y ago
> I noticed as part of a separate discussion over on /r/math that AFAICT there is nothing in PA that distinguishes successor and predecessor until you get to the definition of multiplication. Is that right? Is it noteworthy? I&
701.
by Tainnor 2y ago
So the problem with logic and in particular model theory is that you always have to assume some sort of logic for the world where your models live in (a meta-logic) - otherwise you can't talk about anything. If you take e.g. ZFC for
702.
by Tainnor 2y ago
What is "FINITE"?
703.
by Tainnor 2y ago
Proofs are natural numbers via Gödel's encoding, or any other encoding scheme that you'd like (e.g. ASCII). The sentence "PA is inconsistent" can be stated in the language of PA and it means "there is a number that
704.
by Tainnor 2y ago
I don't know why I wrote an entire proof outlining why first-order PA cannot rule out infinite numbers, if you just ignore it and insist on your misconception. The set of finite numbers is undefinable in the language of first-order PA,
705.
by Tainnor 2y ago
> That seems implausible. All natural numbers are finite. I can easily express that in F.O.L. Just for the sake of clear terminology, I'll take "finite natural number" to mean that it's either 0 or formed by applying
706.
by Tainnor 2y ago
Discussing Gödel in terms of "truth" immediately brings about deep philosophical discussions about what that actually means in the context of mathematics. If the "true" nature of the (standard model of) arithmetic is unk
707.
by Tainnor 2y ago
> It's just that Godel's proof cannot be rendered in PA This is incorrect, the proof can be carried out in very weak subsystems of PA.
708.
by Tainnor 2y ago
PA can model Turing Machines and reason about them. I feel like you missed the important link between logic and computability theory.
709.
by Tainnor 2y ago
You're the only person making argumentative statements. The quoted sentence in the article was descriptive, not normative. In the context where you'd discuss Fourier series, degrees really aren't used. You're the only pe
710.
by Tainnor 2y ago
> To the company this is acceptable noise, but to the individual, this is costing us 100s of thousands of dollars, because there’s only a handful of companies that pay well and they all have the same interview process. If you want to ear
711.
by Tainnor 2y ago
Out of curiosity, have you tried Idris? It would tick at least boxes 2 and 4, while possibly being a little bit more geared towards general programming.
712.
by Tainnor 2y ago
Yeah, that's one of the worst subreddits IMHO
713.
by Tainnor 2y ago
I've only used Lean for proving maths theorems. What do you think makes Lean a better language than Haskell?
714.
by Tainnor 2y ago
> Math seems like low hanging fruit in that regard. First-order logic is undecidable, so no dice.
715.
by Tainnor 2y ago
I don't think I would agree with banning addictive social media platforms, but I would like to see them heavily regulated, meaning: * Opt-in to "engagement algorithms". By default, people should only be seeing things that t
716.
by Tainnor 2y ago
In my case (Lean), I've been getting a lot of help through the Zulip community. There's a dedicated #new_members stream where anybody can ask total beginner questions. It's quite humbling actually when you have someone like K
717.
by Tainnor 2y ago
I'll have to agree with this. In particular, there always seems to be some stage where you'll have to think carefully about how the simplifier works exactly, about different types of equality (syntactic vs. definitional vs. provab
718.
by Tainnor 2y ago
No that's been explicitly disallowed (text messages are notoriously insecure).
719.
by Tainnor 2y ago
I studied maths as a remote degree (after having completed another degree earlier at a regular university), so I didn't have lectures. There were (optional) tutoring sessions (that I didn't make use of) and a few optional in-perso
720.
by Tainnor 2y ago
In Europe, bank transactions have mandatory 2FA. In most cases that means a smartphone apps though many banks also offer a physical device. But you have to pay for the latter, and if you have different accounts at different banks, there&#x2

More ›