Maybe a naive question, but how does one know that a particular lean proof is actually a proof of what one thinks?
Like, ok the logic checks out and it proves something, but there's still the problem of does this logical result actually prove the initial question that was asked?
>there's still the problem of does this logical result actually prove the initial question that was asked?
In math, the question being asked is the validity of a logical statement. That is, there is some rigorous, logical statement which may or may not be true (or even provable, etc.), and the question is whether or not it is actually true or false (or even provable, etc.). Having a proof, fundamentally, means you have a logical statement which only assumes the axioms of the system you're working with and which shows that the statement you're trying to prove is deduced through that statement.
Basically, they already have the "answer" in the sense that the statement they want to prove/disprove/etc. is already known. What everyone doesn't/didn't have is the argument which starts from axioms and leads to that statement which is logically valid. A Lean proof IS this argument. Since it is just logic, it can be checked computationally.
For example, if I assert "2 is an even number," then I haven't proven that 2 is actually an even number yet, but I know that a valid proof of my assertion will end with the statement "2 is an even number". So the question I'd be trying to answer is "what is the line of logic, starting with axioms, which leads to the statement '2 is an even number'"? If I have that line of logic (as a Lean proof), then I can check that it is logically consistent, and if it turns out to be valid, then I can now assert that "2 is an even number" knowing that there is a proof of that statement.
This problem is no different. There is a logical statement corresponding to "Navier–Stokes Millennium Prize Problem" that everyone knows, but which nobody had been able to provide a proof (or counterexample, etc.) for until now.
I was thinking something along the lines of making a mistake when inputing the initial statement, like you wanted to prove that '2 is even' but what you actually stated was that '3 is odd'.
Of course in this simple example it's obvious, but my assumption was that these machine generated lean proofs are millions of lines of code and who knows what they actually say..
You're correct that nobody really understands what these huge Lean proofs actually say. However, the initial statement, even for Navier-Stokes, is not very long [0]. Still, you are also right that sometimes the problem statement can be wrong but it is highly unlikely here.
One wrench to throw into this is that there are a lot of bugs around Lean and they have been incidentally exploited in the past. Hence, we still need a level of human verification today.
Most people in the world wants some form of ethnic cleansing - that's why you get 'ethnic quarters' in most large cities, people generally like to be around their own 'kind'.
Remember, the interrogator is allowed to be hostile, so they would obviously employ all known prompt injections and typical LLM 'gotchas' to figure out who the AI is.
>There's no namespacing feature provided so you're left with the convention of picking a few letters as a prefix and hoping it doesn't overlap and yet is succinct enough to not be annoying.
I've been using C on a daily basis for 30+ years and name collisions has just never been a problem.
Granted, it might be due to lack of a package manager so micro dependencies ala import is_even is not a thing here, but still, in practice, no name collions occurs.
Never quite understood why people are so obsessed with meta programming capabilities in a language, be it templates, comptime, macros, whatever.
I program mostly in C, if I need 'meta' programming I just write another C program that processes C source code (I've written a simple C parser), then in my build script I build in two stages, build meta program, run it, build rest of program.
Simple, effective, debuggable (the meta program is just normal C), infinite capabilities - can nest this to arbitritary depths, need meta-meta programming? Make a program that generates a meta program.
One obvious answer is that people probably don’t want to write a whole parser and wire up new steps in their build pipeline just to do something simple like get the name of enum cases as a string.
Without taking a stance on whether in-language meta programming facilities are good or bad, it’s not hard to find examples of cases where people find it useful to have them.
Actually why even specify metaprogram as C like source code? It must be convenience. But there is little practical use, like a good program always models a lot of different representations of more or less the same things, just recombined and processed a little differently. Why would we want to deal with semantics of C types for example, if we can model a much clearer and better constrained universe of types used in e.g. a de/serialization framework? Even only pointers are quite special, and often only of very immediate use, but there is no point in e.g. persisting them to disk or sending them over the network.
Why would I write a parser that almost-but-not-quite matches the compiler's own parser, when I could just use the compiler's parser directly? I don't want to write a parser, and I especially don't want to debug weird corner cases where my implementation diverges somehow. I just want to write some code that goes like, for each field in T, do X.
C++ metaprogramming is bad, but the problem there is the C++ part, not the metaprogramming-in-the-language part.
Cause its dead simple. Shell out, run a quick sed or something, then compile it in. It is quite amazing what 'magic meta' stuff you can do with that shit. Meanwhile 10 years in we are finally getting reflection.....
Erm... that's not just false. The point of templates is generic programming, reusable components. If you don't put them in a header, you're not reusing them much. And if you have to "selectively pick TUs where they're instantiated", you're basically admitting that you have to invest effort to reduce compile times. You are refuting the very point you're making.
C++ templates _are_ slow to compile. They require running something like a dynamically typed VM in the compiler.
**** Template sets that took longest to instantiate:
833 ms: sf::base::Optional<$> (911 times, avg 0 ms)
Each individual instantiation of this class is sub 1ms.
Including the header itself takes 3ms.
I'm sure I can optimize it even further if I wanted to.
---
Now to refute your other incorrect claims:
> The point of templates is generic programming, reusable components.
That's ONE use case. A more general use case is just reducing code repetition in a type-safe manner, which is extremely useful even within the same translation unit. Another use case is metaprogramming. And I'm sure I can come up with more. Templates are a versatile tool.
> And if you have to "selectively pick TUs where they're instantiated", you're basically admitting that you have to invest effort to reduce compile times.
...well, yeah? Of course you have to put in effort to reduce compile times. That doesn't undermine my point at all.
Not slow to compile? 0,833 seconds extra compile time for a trivial utility class that doesn't do anything interesting other than make something perceived "safer"? Does that mean that each of the 911 instantiations took several million CPU ticks? You could convince me that it's not slow if it was 2-4 orders of magnitude less.
As I wrote elsewhere, 1 second is a timespan where we could aim to compile 1 MLOC of code on a single core.
> A more general use case is just reducing code repetition in a type-safe manner
As I said -- code reuse. And interestingly your Optional.hpp is a header...
That's a strange dismissal. `Optional<T>` isn't "perceived" safety -- it eliminates a whole category of bugs (null dereferences, uninitialized reads) at the type-system level, with zero runtime overhead versus a raw pointer or sentinel value.
If you think that's uninteresting, that's an aesthetic preference, not a technical argument.
But let's set that aside, because it's also irrelevant to the compile-time claim.
The point of the example wasn't "look at this fascinating class," it was "here is a real template, used 911 times across the codebase, in a public header -- exactly the scenario you said would be slow -- and it costs under 1ms per instantiation."
You can swap `Optional` for any non-trivial template of similar complexity and the numbers will look similar.
On your 1 MLOC/sec benchmark: that's a fair reference point for C-like code, but it's not the right yardstick for template instantiation, which is doing semantic work (overload resolution, SFINAE, constraint checking) that a C compiler simply isn't.
Comparing them is comparing different jobs.
The honest question is whether template compilation is slow relative to what it's actually doing, and in well-structured code, it isn't.
And yes, `Optional.hpp` is a header -- that's the whole point of the demonstration. I'm not claiming you should hide every template in a .cpp file. I'm claiming that even templates in headers, instantiated hundreds of times, are cheap when written with compile times in mind.
The "put templates in .cpp where it makes sense" advice is for the specific cases, not a blanket rule.
In practice, C means you end up with generic data structures with pointers to what they contain, rather than being inline.
You do see a lot of macro use to deal with this, but that is just primitive, non-typesafe metaprogramming, and it gets unwieldy enough that in practice, you see people add an extra pointer. This is why it gets slower.
In practice, I see people write very performance C code where it matters, while moving on quickly where it does not. C++ code is often highly templated with annoying compile times, but still often slow because it still does not use the right data structures, and the amount of instruction bloat by specializing everything does not help for anything which is not a toy benchmark.
If you need callbacks and generics, you're not writing performance code.
99% of code in the wild is comically inefficient and is doing the wrong thing, using way too generic data structures and algorithms for very concrete problems. C++ templates may be one way to make comically slow code faster by spending a lot of compile time. But it's often much quicker to just write straightforward concrete code that the compiler can easily optimize.
IMO C++ makes for slow programs for the sole fact that it compiles so slow (if you use its modern features), so you have much less time to actually iterate and improve.
If compilation is even more than 10% of the time it takes you to run your tests, you're probably not writing correct code. Compilation times don't even measure.
So every time you compile, you run your test suite? I don't. And you trust that I have experience writing and compiling programs too...?
It should be a goal to keep rebuild times around 1 second (often not quite possible, but 3-5 seconds, even for full rebuilds, is often realistic). I edit, compile, run, edit, compile, run. Editing and running can often take as little as 1-3 seconds, and I sometimes do it dozens of times working in a row, working on a single improvement. That's why there is a 1 second rebuild time goal.
In practice I often work on codebases I don't fully control, but when the build times are excessively high, I will complain and try to improve. Build times longer than 10-15 seconds break the flow, they are a significant productivity hit. But they are quite common with C++ codebases (it can also be bad with C codebases by the way, but C++ is typically much worse because of templates and metaprogramming which is very slow).
You run your code before running tests? IMO that's bad practice.
1 second, seriously? Even the Linux kernel is based on C, and it doesn't even have compilation times approaching that.
I guess I also work on a lot of big data projects, where getting results will take... 48 hours or so, so anything shorter than that is basically some sort of unit test or dry run... so in that context, compilation times do not even register on the things slowing me down.
Running the code immediately after making changes is the first line of testing. To run a huge test suite full of tests that are completely unrelated to the current changes would be stupid, it's a huge waste of time and energy.
Yes, seriously, have you ever written a project from scratch? A simple .c file with a thousand lines in it should easily build and start within 100ms. A compiler should be able to do basic parsing and codegen at 1M lines per core.
If your runs take 48h, of course you need a strategy to avoid noticing bugs only after dozens of hours running. You can't tell me that it is efficient to make changes and to wait for minutes or even hours before noticing that your code wasn't even syntactically valid, or maybe it did compile but your code had a small oversight and you need to start over building.
The Linux kernel is a HUGE project, one of the biggest around. Yes, a full rebuild takes a long time, depending on configuration. Incremental rebuilds do not, though.
I'm actually working on a Linux kernel module (distributed filesystem client), it's on the order of 40 KLOC. I can do a full rebuild in 10/15 seconds (debug/release), and that includes calling into the kernel's infrastructure and doing a lot of stuff that shouldn't have to be done. An incremental rebuild after changing a single .c file is about 3 seconds. Restarting the module (swapping for the newly built one) takes less than 10 seconds also. And this can be already a stressful bottleneck depending on the task. Say you're improving logging in a particular section of code, this can easily require 5-10 attempts.
I'm working on Desktop GUIs (2D/3D) too. You need a quick turnaround time as much as possible. Many changes are trivial but you want to do many small incremental improvements, recompile, run and test (manually), often with a breakpoint on the code you're currently working on.
The projects I'm working on are written in C or conservative C++, and most have from thousands to hundreds of thousands lines of code. They can be built from scratch in a short amount of time (< 10s for the smaller ones). And all of them do incremental builds in <= 10 seconds except when maybe changing the most central headers which essentially means a full rebuild.
You can also design a C/C++ codebase to always do a full rebuild, compiling everything as a single unit. That can be faster than trying to do incremental builds, for codebases of considerable size. Try out the popular raddebugger project, a complete build after checkout is about 3 seconds. It's ~300 KLOC I think.
It really depends on what you are doing. Sometimes I am not building in a day, just designing and thinking by editing. Sometimes I am refactoring for hours without building. But sometimes I am rebuilding every 10 seconds or so.
Writing a C++ parser is much harder than a C parser to the point there had been just 3 parsers used among all C++ compilers for quite a while. So you'd need to use some library for parsing. So now you are looking into the library's parser compatibility with the compiler you are using (it might not support the C++ standard you are on at all, it can have bugs preventing it from parsing the code that the compiler parses just fine) and not just on your code but on the library headers you include in your code. What are you going to do when cindex/libclang or whatever chokes on a libstdc++ header? You also have the issue with builtin macros: are they are the same in your library parser? Most likely not. Good luck testing all that.
Two-stage compilation is just a bonus on top: you add a sequential dependency in your build graph and if you have enough of these parsing programs you are going to wait till they are all built before your build can go wide.
Usually destructors can't fail. But for rare cases like with close() you can write a helper function (static method) which destroys the given object and returns an error if has one.
One reason is that c++ still hasn't gotten 'trivial relocatability' right - i.e being able to memcpy/memmove and not have to call constructors/destructors when growing your vector class.
Actually, issues with non-trivial moves and relocations are specific only for C++. Some other languages (notably Rust and Swift) don't have such issues, but still have nice automatic memory management via destructors and containers atop of it.
C++ compilers optimize-out empty destructor calls and sometimes even replace calls to move constructors/move assignment operators via memcpy. But it's unfortunately not guaranteed in all cases due to constrains of the C++ object/memory model designed initially without proper move semantics.
reply