markusde

8 ms·

31.
by markusde 2y ago
This is 100% the case. All of the honest-to-god Rust experts I know work on the compiler in some way. Same goes for Lean, which bootstraps from C as well.
32.
by markusde 2y ago
Unlike curing cancer, the IMO problems were specifically designed to be solvable
33.
by markusde 2y ago
I've also heard quite a few people saying that their PhD was one of the best times of their life, because of how free they were to pursue things they found interesting (many of them have also settled down with a family, as well). Diffe
34.
by markusde 2y ago
Not much. It's too inaccurate for my research and is a bad writer. Day to day I write Lean, and I use moogle.ai to find theorems. It's... fine as a first pass. The website constantly gets confused about similar-looking theorems, i
35.
by markusde 2y ago
> describe 0% of the rational numbers between 0 and 1 I think you mean irrational :)
36.
by markusde 2y ago
Fair enough, I haven't used many proof assistants without dependent types, and I probably should.
37.
by markusde 2y ago
But with coercions you do have {↑n | n ∈ ℕ} ⊂ ℤ, which is the subtype that you really want! The issue is that not all properties of subsets can be lifted to supersets. As an example from analysis, you can coerce the reals ℝ to the extended
38.
by markusde 2y ago
It doesn't matter but I fully disagree with this. A transpiler emits code the user is supposed to understand, a compiler does not. At least that's the general way I've seen the term used, and it seems quite consistent.
39.
by markusde 2y ago
I noticed this in myself last time I was as a TA. I'd go back and re-grade the first 15 assignments or so to make sure the rules were being applied consistently.
40.
by markusde 3y ago
I would also be interested in reading some of these examples!
41.
by markusde 3y ago
Yes... Rust! I don't know if you can toggle it from the front-end, but the Polonius borrow checker includes a "location insensitive" mode which is faster but accepts fewer programs.
42.
by markusde 3y ago
The difference is, a junior employee knows that killing prod is bad. An LLM doesn't know anything.
43.
by markusde 3y ago
I chased some links from Wikipedia and you're right that Edmonds uses "efficiently solvable" to mean P. However, he does not take "efficiently solvable" to mean "feasible" for basically the same reasons as
44.
by markusde 3y ago
I am a theorist (though not in complexity) so I agree with you that new math is never bad. I also agree that an very lucky P=NP result _may_ be implementable _at some point_ in the future, though to be honest I wouldn't put my money on
45.
by markusde 3y ago
That's not Cobham-Edmonds thesis. The assertion is that problems are feasible _only if_ they are in P, not _if and only if_ they are in P.
46.
by markusde 3y ago
Ok. When I say efficient, I mean "produces efficient code on near-term hardware". I understand that complexity theorists have a different definition of "efficient"-- they also have a different definition of "importa
47.
by markusde 3y ago
Even a P=NP result doesn't tell us that NP problems have efficient solutions. That depends entirely on - if the solution is constructive, - if the asymptotic solution has good constants (lower bound on input size, highest degree term),
48.
by markusde 3y ago
I disagree that this is an important problem. Even in the unlikely case that some NP-hard algorithm is P, it may be completely infeasible to compute on modern hardware. I'd wager that to certainty be the case if any solution exists at
49.
by markusde 3y ago
Full verification is one, but that is still challenging at scale. Formal methods has many weaker methods as well which are easier to apply in general (automated proof, abstract interpretation, static or dynamic model checking, hell some wou
50.
by markusde 3y ago
How's this for interesting: many people in my field (formal methods) seem to be pretty excited about our job prospects. Before we used to just say that people don't actually know what their code does, but now it looks like it migh
51.
by markusde 3y ago
A problem with randomly searching for theorems is that it blows up exponentially, and many of the theorems you would find are probably not useful in their own right. Another problem is that "check the for truth" is undecidable: th
52.
by markusde 3y ago
You're mixing up functional programming with an execution model for functional languages. These are not the same.
53.
by markusde 3y ago
It's not absurd because nobody is forcing that person to rent. Housing is a public resource, and contributing to that public resource shouldn't come without asterisks. Cities need the non-owning class to function, and cities funct
54.
by markusde 3y ago
This is slightly misleading. "All of science" doesn't rely on intuition-- it relies on the scientific method. Intuition guides how we develop our models but ultimately there _is_ a real forcing function in the sense that the
55.
by markusde 3y ago
IMO pure FP is nice because _compositionality_ is nice. If my problem has lots of simple data structures that represent mathematical objects, then usually I find that most of things I want to do with them can be succinctly modeled with pure
56.
by markusde 3y ago
That's a good way to put it! Town squares sound great, but every city square I've been in is full of yelling and pickpockets.
57.
by markusde 3y ago
I get your point, and I agree with it too. My comment is (trying to) say that in those cases we don't know that humans are any better! Your other comment has some problems, but a better example is fn collatz(mut n: bigint, mut v: Vec&l
58.
by markusde 3y ago
It's not verifiable because you're trying to prove an incorrect spec! This program's memory usage is _not_ bounded above by a constant! However, many modern formal methods _could_ prove that this function uses `f(x)` space, p
59.
by markusde 3y ago
This is a good but also misunderstood point. It is true that you can't automatically do this in general. However, expressive enough type systems can contain human-written, machine-checked proofs of (models of) these properties. I think
60.
by markusde 3y ago
Agreed. At my undergraduate we didn't have an equivalent, and a common complaint amongst the TA's was how little concrete devops skills the students had. One of my friends TAing a second year course even went so far as to say almo

More ›