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.
209 karma · joined October 2, 2021
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, it can't pattern match, and it can't really introspect typeclasses (which can be hiding the theorems I want). However it usually can usually help me go from a vague description of what I want to some relevant doc pages, so credit where it's due for that.
I think you mean irrational :)
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 reals ℝ∞, but you lose some of your rewrite rules because you need to choose how to define edge cases like (∞ - ∞) in ℝ∞. Making these choices is common in mathematics (at least in analysis) and in pencil and paper proofs it's usually just handwaved away.
Using subtypes, a proof checker would have to be explicitly given which ambient superset you're going to rewrite something like ((a : ℝ) - (b : ℝ)) in... this is more or less the same as using coercions to distinguish between ℝ and {↑r | r ∈ ℝ} ⊂ ℝ∞ except with subsets type inference is way harder.
I'll admit that coercions are annoying, but subsets don't let you get around it: here there's an essential step up in complexity between sloppy pencil and paper proofs and verified code. Personally, I'm really interested in seeing how much of mathematical handwaving can be rigorously automated away. There's a lot of cool work in this area by I don't think the FM community has a definitive answer for it yet.
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.
> An explanation is due on the use of the words "efficient algorithm." First, what I present is a conceptual description of an algorithm and not a particular formalized algorithm or "code." For practical purposes computational details are vital. However, my purpose is only to show as attractively as I can that there is an efficient algorithm. According to the dictionary, "efficient" means "adequate in operation or performance." This is roughly the meaning I want—in the sense that it is conceivable for maximum matching to have no efficient algorithm. Perhaps a better word is "good."
> It is by no means obvious whether or not there exists an algorithm whose difficulty increases only algebraically with the size of the graph. The mathematical significance of this paper rests largely on the assumption that the two preceding sentences have mathematical meaning.
> ...
> When the measure of problem-size is reasonable and when the sizes assume values arbitrarily large, an asymptotic estimate of FA(N) (let us call it the order of difficulty of algorithm A) is theoretically important. It cannot be rigged by making the algorithm artificially difficult for smaller sizes. It is one criterion showing how good the algorithm is—not merely in comparison with other given algorithms for the same class of problems, but also on the whole how good in comparison with itself. There are, of course, other equally valuable criteria. And in practice this one is rough, one reason being that the size of a problem which would ever be considered is bounded.
You should read the rest of section 2, it's short very clear. Calling P the class of "efficiently solvable" problems is a completely reasonable framing for this paper, considering that this was written at a time when we had fewer tools to formally compare algorithms. Edmonds correctly does not claim that all P algorithms are feasible, and my opinion that P=NP is not important is based on the 60 years of feasible non-P computations we've had since.
As for more important problems-- I think it's more important to improve the specializations of NP problems, heuristically, for problem instances which arise in practice. A concrete example in my line of work could be improving the performance of SMT solvers on encodings of real programs. There's a lot of exciting work happening in this area and it's opening doors in program verification previously thought to be unrealistic. IIUC the formal methods team at AWS is putting a lot of work into memoized, distributed SMT solving, and are making meaningful gains over the current state of the art.
I don't really care if we can solve the most general NP hard problems in O(bad*N^bad) only for N>bad. A) Even a getting result that weak seems to be too challenging to prove and probably not true, and B) trying to solve the most general problem is complete overkill for any problems that come up outside a complexity textbook.
- if the solution is constructive,
- if the asymptotic solution has good constants (lower bound on input size, highest degree term), and
- having no other mitigating factors (requiring absurd amounts of space, for example)
The idea that P=efficient is a complete misnomer. For simple algorithms, asymptotic analysis is a fine enough coarse-grained view of program performance. However for extreme cases (like may be the case for P=NP) asymptotic analysis tells you almost nothing at all.
I am not aware of any practical use of P=NP outside of pure complexity theory, and the P!=NP case is already ubiquitous assumption anyways. P=NP would be a notable result, but probably not important.
I think that a shift from "this is my program, it's a sequence if steps that does what it does" to "I asked a LLM to generate me a program that does this vague thing I want" makes you naturally ask questions like "wait is it actually doing the thing I want" and "what do I even want it do do". Formal methods, broadly, has a lot of good answers to those questions.
Cities need the non-owning class to function, and cities function better when the non-owning class has some degree of stability-- letting landlords juice their tenants for as much as possible is counterproductive to this.
An example of why this matters: string theory. AFAICT It's a field that is built with a clear(ish) intuition and rigorous use of logic, but because it is experimentally unverifiable the field has never really moved past conjecture.
This property is true to varying degrees outside of pure FP too. For example in Rust I find that expression-orientation makes programs fairly easy to compose, modulo thinking about ownership.
Town squares sound great, but every city square I've been in is full of yelling and pickpockets.
Your other comment has some problems, but a better example is
fn collatz(mut n: bigint, mut v: Vec<...>) {
loop {
n = { if n%2==0 then n/2 else 3\*n+1 };
v.push(...);
}
As far as we know, we can't bound the memory usage of this program: and if any FM can do it as well then there's a million bucks on the table. But so far no human can do it either! And if your program relies on this program using bounded memory, from an engineering perspective you're kind of SOL no matter what.
On the other hand, if you're writing programs which humans are pretty sure they know why the properties they want hold (as we usually try to do, anyways), then translating this into a machine-checked proof can give you a lot more faith that the property actually holds and possibly even find flaws in your reasoning/implementation if there are any!
However, many modern formal methods _could_ prove that this function uses `f(x)` space, provided the loop body is simple enough.
The way I see it formal methods not a holy grail where we don't have to think about the code we're writing anymore, but it is a very strong next step from "I wrote this code and here's why I think it's right" to "I wrote this code and here's a machine-checked proof that it's right". Effective automation can make that step easier to take in a lot of real-world cases.