Tainnor

12 ms·

121.
by Tainnor 1y ago
> but that's not a general theorem prover at that point, that's a theorem classifier for a specific formal theory (namely ZFC). huh, no, it will work just as well for any FOL theory with a recursively enumerable set of axioms,
122.
by Tainnor 1y ago
> The halting problem disproved excluded middle. That's a weird category error.
123.
by Tainnor 1y ago
My pet peeves when it comes to undecidability: 1. People saying "sure, problem A may be undecidable but it's decidable for instance X". That's not how the concept works - if you restrict the a problem to a specific insta
124.
by Tainnor 1y ago
> Any axiomatic system will have true statements that are unprovable. Any effectively computable axiomatic system of sufficient strength. The "effectively computable" condition is probably uninteresting (if we couldn't eff
125.
by Tainnor 1y ago
You're mixing things up. By a "general theorem prover", we typically mean "a program which can decide for every sentence in FOL whether it's valid" (I say FOL, because the situation is even worse for HOL), i.e.
126.
by Tainnor 1y ago
Decidability is a term from theoretical CS where languages can be arbitrarily big. It doesn't make sense to repurpose the term for actual finite-memory machines.
127.
by Tainnor 1y ago
> Let F be a field, and let a,b∈F such that ab=0. There are two cases to consider: a=0 and a≠0. If a=0, then indeed ab=0 by Proposition 1. This part is a bit weird. If a=0, then we are already done, there's no need to prove ab=0 (wh
128.
by Tainnor 1y ago
A debugger will also allow you to step through library and framework code where you can't usually go and place print statements.
129.
by Tainnor 1y ago
No, I do not agree. Which languages are vanity projects in your eyes?
130.
by Tainnor 1y ago
> But developers found a way to gatekeep the whole process by inventing thousands of different languages/wheels over time. Yep, definitely would have been better if developers hadn't invented higher level languages and LLMs wou
131.
by Tainnor 1y ago
As much as I find Haskell elegant for many things, I have to agree. It reminds me of the infamous Haskell "quicksort" which isn't actually quicksort because it's not in place. I think not every piece of code needs to be
132.
by Tainnor 1y ago
It doesn't have to be a general purpose CSV parser, it just has to be able to parse the specific AoC input
133.
by Tainnor 1y ago
Given that Java is one of the most used languages globally, 10% of it is still significant. It's definitely easier to find a (backend dev) job using Kotlin around here than one using Elixir, Common Lisp or Haskell, yet I don't see
134.
by Tainnor 1y ago
I don't care about the market size as long as it's big enough that I can find jobs, which I can. Also no idea how the links you posted are supposed to support your assertion that Kotlin is chosen due to code sharing considerations
135.
by Tainnor 1y ago
> Most shops that use Kotlin on the backend also do Android development, as means to do core sharing between backend and Android None of the companies that I wrote Kotlin for or that I applied to used Kotlin for code sharing between back
136.
by Tainnor 1y ago
Same in Germany, there are a lot of major companies using Kotlin for backend code.
137.
by Tainnor 1y ago
To be technical, "accusative" etc. are cases (i.e. forms of words) while "direct/indirect object" are grammatical roles - those are different categories. In German, for example, the Dative case can mark an indirect
138.
by Tainnor 1y ago
I do think English has deviated more from its Germanic roots due to the pervasive influence of French (there are people who call English a creole although I think that's taking it a bit far). But I agree that languages with more comple
139.
by Tainnor 1y ago
In every country there will be some expat bubble which can get away with not learning the local language(s). Sometimes that bubble will be bigger and sometimes smaller, but it definitely exists in Germany too (mostly in Berlin). That said,
140.
by Tainnor 1y ago
> The Latin-derived cases They're not Latin-derived, they come originally from Proto-Indo-European (which had even more cases). Many other Indo-European languages retain cases (Slavic languages, Greek, etc.), but were lost in Englis
141.
by Tainnor 1y ago
It's true that English uses basically the same method to create compound nouns, but quantitatively it's a difference. Long compounds consisting of 3, 4 or more parts are completely common in German and cause usually no trouble in
142.
by Tainnor 1y ago
Weltschmerz and Bildungsroman relate very closely to their compositional meaning. Sure, they have become slightly more specialised (a novel about a teacher wouldn't be a "Bildungsroman", I guess), but it's not like you c
143.
by Tainnor 1y ago
> ORMs Certain ORMs such as Rails's ActiveRecord are part of the problem because they create the illusion that local memory access and DB access are the same thing. This can lead to N+1 queries and similar issues. The same goes for
144.
by Tainnor 1y ago
Prevent forced pushes on protected branches (develop, main, hotfix etc.). I don't care if somebody force pushes their private feature branch.
145.
by Tainnor 1y ago
No idea why you're picking on the author's minor grammar mistakes. They may not even be a native speaker. The article is perfectly understandable, I read it myself and didn't even notice the errors before you pointed them out
146.
by Tainnor 1y ago
did you read the wrong article?
147.
by Tainnor 1y ago
I have a pet (undergraduate complex analysis) formalisation project in Lean, purely for didactic and recreational purposes. I find it rewarding in the same way others may find it rewarding to train for a triathlon - it's often extremel
148.
by Tainnor 1y ago
I didn't edit my original comment. Compilers are totally besides the point. Python, Java and even Prolog aren't FOL, they lack its expressive power.
149.
by Tainnor 1y ago
OP specifically asked for a program that would derive code from logical specifications, not a run-of-the-mill compiler where you have to write the code yourself (albeit on a higher level). If your specification logic is strong enough to enc
150.
by Tainnor 1y ago
> try a few easy leetcode problems in Lean with a proof of correctness This might actually be harder than, say, proving some undergraduate math theorems because reasoning about mutable state (especially when you want it to be performant)

More ›