I broadly agree with your sentiment and am saddened (outraged?) to see the financially motivated cheapening of (destruction of?) what mathematics truly is. I agree that formal logic is merely a model of one aspect of what mathematicians do, in the same sense that a computer simulation of a roller coaster can never bring the same value to us as the real thing.
However, I would be remiss if I didn't question your historical claim, which seems to me a bit too strong:
> Mathematics predates the idea of formal proof by millenia [...] Formal proof only emerged early in the 20th century [...]
You seem to associate the start of "Mathematics" with Euclid, but (as far as I know) he worked at approximately the same time as Aristotle. Aristotle's syllogisms are perhaps the most famous formal logic system: their correctness relates only to their form, not their content. All deductions of the form "All X are Y, All Z are X, hence All Z are Y" are valid (assuming the premises are), regardless of the meanings of X, Y, and Z. (Outside of Greece, my understanding is that a few hundred years earlier Panini had also developed a system of formal manipulations, but for representing grammars.)
What, to my understanding, "emerged" only the 19th and 20th century was 'merely' a formal logic both expressive and sound enough to properly express modern mathematics (the Beggriffsschrift in the 19th century and FOL+ZFC in the 20th). Between Euclid and the 19th century the development of calculus was probably the biggest advance in mathematics, and my understanding is that Leibniz himself spent significant time working on formal logic.
Perhaps I have the wrong definition in mind of 'formal logic' or 'mathematics,' but I do think the history of formal logic is much more closely tied to the history of mathematics than your post makes it seem on first glance. Though I certainly agree that "mainstream mathematics" has never felt it necessary (or necessarily that useful) to express proofs in a formal logic carefully enough that they could be checked by computers; this was a fringe focus of a minority group of mathematicians and computer scientists that was co-opted as a marketing stunt into 'what mathematics is' for major corporations trying to justify their money burn.
The idea that logic is a branch of mathematics is itself a modern notion. Aristotle's logic was part of the trivium (grammar, rhetoric, and logic) in classical notions of education, while mathematics made up several parts of the quadrivium (arithmetic, geometry, music, and astronomy).
Of course in retrospect we can see that the syllogistic part of Aristotle's logic can be formalized (as can grammar), but it was viewed as part of language or philosophy. I get the impression that a lot of more traditional philosophers of logic hated the formal turn.
Leibniz anticipated the turn towards formalism, but he didn't publish any of it in his life and it wasn't rediscovered until the 20th century.
Knowing some folks that work on "major-browser-vendor" security in the era of Mythos-found-and-exploited vulnerabilities everywhere, the thought of running completely random untrusted Javascript on my machine has freaked me out to the point that I run NoScript on all of my machines now.
I've found NoScript actually very usable, as long as you allow yourself to be fairly liberal in marking domains "trusted." I only truly routinely visit a core 10-20 domains that require Javascript, and they're from "reputable" organizations (my bank, employer, etc.) so those all get marked "trusted" quickly and I don't worry about them going forward.
In the "long tail" of random things I click on from HN links, seeing a "You need to enable Javascript to view this app" message is actually a fairly good signal that I don't want to view that app (though you might be surprised how many websites are browsable comfortably---or even more comfortably!---without JS enabled).
One thing I wish NoScript supported was the ability to mark a domain as a "trusted page domain" in the sense of: "HTML served from this domain can load scripts from any domain" (rather than trust being assigned to the domain serving the script itself). Perhaps it has this feature and I just haven't found it.
I do the same exact thing, except I disable JavaScript for all sites by default in uBlock Origin.
Same experience as you, also: many sites actually work well enough without JavaScript, and the ones that do require it to display anything make me pause and ask if I truly want to give that site the privilege of running code on my computer. Majority of the time the answer is no.
> also: many sites actually work well enough without JavaScript
Some work better without JS. The most common are information-based sites with a paywall or signup or whatever. The JS loads some huge wall over the content. Bonus, no cookie popups or another annoyances, and most ads are loaded with JS. Popups are getting ridiculous.
The AdminVM is based on Fedora and has systemd, but it has no network and you you shouldn't run anything there. Unless you think that systemd is actively malicious and specifically targets Qubes, any vulnerabilities in it are not exploitable.
> Knowing some folks that work on "major-browser-vendor" security in the era of Mythos-found-and-exploited vulnerabilities everywhere
Is this a thing now? I hadn't seen any big browser vulnerabilities recently. Did I miss something? Or are the vendors not releasing horrifying bugs they found internally with AI fuzzing?
It's never clear what's "real" vs. marketing for the LLM companies, but Mozilla at least has made a big deal publicly about the "unprecedented" number of "latent security bugs" they've found using tools like Mythos:
To be honest, I'm not sure how many (if any) of them have actually been exploited, but in any case, it seems like the cost to at least find a vulnerability anymore has really dropped dramatically.
I'm seriously strategizing how to best run a separate user-account for banking etc., to defend against a user-level compromise of my day-to-day stuff.
It seems like anything that involves sharing a desktop window (e.g. xhost tricks) is not really security worth the effort, I've got to at least stop block any malware that monitors the screen, clipboard, keystrokes that come after the phrase "sudo", etc.
Being taught this rule in undergrad really hampered my appreciation of C. As I've said in a previous comment, the real key that unlocked understanding C declarations for me is the mantra "declaration follows use." You declare a variable in C in exactly the same way you would use it: if you know how to use a variable, then you know how to read and write a declaration for it. Once I understood this elegant idea, it became hard to enjoy using statically typed languages that eschew it.
Call me a hater but I don't like the spiral rule and I like "declaration follows use" even less.
How do you make an std::array of a given type? Wrap the existing type in an extra layer of std::array, we all know this, it makes sense, there's no reasonable alternative. How do you make a C-array of a given type? Oh boy, "prepend the array specifier before the list of existing array specifiers" (actually it's worse because you have to find the right possibly-empty array of existing array specifiers first, just because there's a list of array specifiers somewhere in the type doesn't mean it's the one you should be prepending to).
"Declaration follows use" immediately goes out the window when faced with typedeffed types being used as the base type, or (as mentioned) generics in descendant languages of C. Instead you get "declaration builds up a type by wrapping layers around a core, use breaks down a type layer by layer starting from the outside" (so, necessarily, they mirror each other). C could have worked that way, and it would have made more sense.
"Declaration follows use" is the type level equivalent of taking off your socks before taking off your shoes because that's the order in which you put them on.
> we all know this, it makes sense, there's no reasonable alternative
There absolutely are reasonable alternate ways to represent ordered data that don't involve templates. The way that C does it makes sense in most cases, and if you are looking at something that you cannot understand, you are looking at bad code.
> "Declaration follows use" immediately goes out the window when faced with typedeffed types being used as the base type
Typedefs are an abstraction. If you create a typedef, it is usually because you only want to handle the data as a whole, passing it to helper functions that remove the typedef. Also, declaration of use does not break down with typedefs:
> "Declaration follows use" is the type level equivalent of taking off your socks before taking off your shoes because that's the order in which you put them on.
Please give me an example of some C code where this is the case.
No, I think he means that for any given type, you can wrap it in an array the same way. Your example is demobstating that it even works recursively, but it works in the simple case too by wrapping "int" in an array to get an array of ints. There's no need to jump back and forth between each side when adding new layers (which gets described as a "spiral", but in a single line of code, I'd argue that it's really just jumping back and forth, and that's why it's annoying to people like the parent commenter and I)
Yes, if you only use arrays, then it doesn't make things confusing. The point they were making (as I understand it) is that putting a pointer inside std::array doesn't change the way you have to read it, which is not the case for C arrays.
means that `*w` is an `int`, meaning `w` is a pointer to an `int`.
int *y[5]
(note that `◌[]` has higher precedence than `*◌`, so this is `*(y[5])`) means that `*y[5]` is an `int`, so `y[5]` is a pointer to an `int`, meaning `y` is an array of `int` pointers.
int (*(*kitchensink[5])(int, int))[6];
means that `(*(*kitchensink[5])(int, int))[6]` is an int, so
- `*(*kitchensink[5])(int, int)` is an array of `int`.
- `(*kitchensink[5])(int, int)` is a pointer to array of `int`.
- `kitchensink[5]` is a function pointer to a function that takes `(int, int)` and returns a pointer to an array of `int`.
- `kitchensink` is an array of function pointers to functions that take `(int, int)` and return a pointer to an array of `int`.
I think this is a valid point. I would much prefer if the spiral rule were presented as a helpful mnemonic for remembering C operator precedence rather than something uniquely connected to declarations!
> When I was in mathematics, reading other people's work was always more rewarding to me than doing my own. [...] I really welcome the omniscient mathematician machine people are predicting.
Curious, as someone who relates strongly with both the OP and your first sentence: did it matter that you were reading "other people's work?" Or was it simply the satisfaction of understanding an answer?
Personally, one of the things that finally drew me to math as an undergrad (vs. high school where I thought of it as a stupid competition played by people who cared too much about showing off their smarts) was an instructor who helped me think of studying math as a conversation with a fellow human being many miles, centuries, languages, and cultures removed from me. Despite that distance, my mind was appreciating a creation that another human had cared for and poured years of their life into. There was a sort of romance to it, like the feeling of butterflies-in-the-stomach we get from seeing a multi-thousand-year-old cave painting, yet even more impressive because of the depth of the thought communicated.
I personally haven't been able to recreate that feeling from computer-generated math. Whenever I try to, I feel deeply uncomfortable (somewhat similar to the thought of eschewing human connection for an 'AI companion').
I'm more optimistic than the OP, especially when I think of new discoveries in healthcare. And I know there's enough "organic human-created math" from the last ~2k years that folks who feel the way I do can spend the rest of our lives studying only that. But it is sad to think that this multi-thousand-year project of "communicating human mathematical creations through time" has just ... ended? Or seems to be ending soon? Or at least greatly cheapened from a romantic dream into a sort of fun hobby, like recreational knitting? I can't help but share the OP's sadness that something seems to have been lost for future generations. Though a lot has been (and will be) gained as well, for sure!
It does not matter to me. As long as the prose is good and the arguments are well-exposed I don't mind if an AI wrote it or a human. It would be different if we were talking about music, art or literature. But for science I care about the content, not who created it. The social aspect of mathematics was never alluring to me.
Since this is about C declarations: for anyone who (like me) had the misfortune of learning the so-called "spiral rule" in college rather than being taught how declarations in C work, below are some links that explain the "declaration follows use" idea that (AFAIK) is the true philosophy behind C declaration syntax (and significantly easier to remember/read/write).
TL;DR: you declare a variable in C _in exactly the same way you would use it:_ if you know how to use a variable, then you know how to read and write a declaration for it.
Using x, or dereferencing p, or subscripting the array arr, or declaring a function that can be called with fn, or dereferencing the function pointer pfn then calling it, all these things would produce an int.
It's the intended way to read/write declarations/expressions. As a consequence, asterisks ends up placed near the identifiers. The confused ones will think it's a stylistic choice and won't understand any of this.
Yes, the () operator dereference function pointers automatically for you for convenience. There's also the surprise that you can infinitely dereference function pointers as they just yield you more function pointers.
One baffling thing I see people do with typedefing function pointers is insisting on adding in the pointer part in the typedef which just complicates and hides things.
If you want to typedef a function pointer, make a completely ordinary function declaration, then slap 'typedef' at the beginning, done.
This does require you to do "foo_func *f" instead of "foo_func f" when declaring variables, but that is just clearer imo.
typedef int foo_func(int); // nice
typedef int (*foo_func)(int); // why?
I once considered Wren for a situation where I (to a first approximation) wanted to allow users to write 'plugins' that link against my internal C application symbols but using a language focusing more on ease of use (rather than C).
Unfortunately, neither Wren nor any of the other major 'embeddable scripting languages' (e.g., Lua) were really a good fit for this, because they commit fully to the 'all-numbers-are-floats' thing and generally don't seem to even try to provide a general equivalent to the C++ `extern "C" { ... }` thing.
Of course, I know this isn't really the target use case of Wren/Lua/etc., but if anyone knows of a good embeddable scripting language for this I'd love to hear about it. Eventually I went with CPython (which provides ctypes to solve my problem) but it's a huge pain to embed properly.
LuaJIT does provide C-compatible types through its FFI. I generally prefer LuaJIT over normal Lua for this reason. It also makes embedding super trivial as you only need to use the Lua API to bootstrap and call the first Lua function, after that you can just use the FFI which lets you work directly with extern host functions.
Ones that might be of interest to you are Umka, tcl, and berry.
There's also a lot of others listed that range from someone's experimental side project to professional grade and well supported languages. Kinda fun to see different people's approaches to things, and no matter what your preferred programming style, there's probably a few in there that will mesh pretty well.
Given the goal is to work with existing C programs (which already have free(...) calls "carefully" placed), and you're already keeping separate bounds info for every pointer, I wonder why you chose to go with a full GC rather than lock-and-key style temporal checking[1]? The latter would make memory usage more predictable and avoid the performance overhead and scheduling headaches of a GC.
Perhaps storing the key would take too much space, or checking it would take too much time, or storing it would cause race condition issues in a multithreaded setting?
I think the lock and key approaches don’t have Fil-C’s niftiest property: the capability model is totally thread safe and doesn’t require fancy atomics or locking in common cases
Also find it interesting that you're allowing out-of-bounds pointer arithmetic as long as no dereference happens, which is a class of UB compilers have been known to exploit ( https://stackoverflow.com/questions/23683029/is-gccs-option-... ). Do you disable such optimizations inside LLVM, or does Fil-C avoid this entirely by breaking pointers into pointer base + integer offset (in which case I wonder if you're missing out on any optimizations that work specifically on pointers)?
For starters, llvm is a lot less willing to exploit that UB
It’s also weird that GCC gets away with this at all as many C programs in Linux that compile with GCC make deliberate use of out of bounds pointers.
But yeah, if you look at my patch to llvm, you’ll find that:
- I run a highly curated opt pipeline before instrumentation happens.
- FilPizlonator drops flags in LLVM IR that would have permitted downstream passes to perform UB driven optimizations.
- I made some surgical changes to clang CodeGen and some llvm passes to fix some obvious issues from UB
But also let’s consider what would happen if I hadn’t done any of that except for dropping UB flags in FilPizlonator. In that case, a pass before pizlonation would have done some optimization. At worst, that optimization would be a logic error or it would induce a Fil-C panic. FilPizlonator strongly limits UB to its “memory safe subset” by construction.
I call this the GIMSO property (garbage in, memory safety out).
Not knowing the exact language used by the C standard, I suspect the reason GCC doesn't cause these issues with most programs is that the wording of "array object" refers specifically to arrays with compile-time-known sizes, i.e. `int arr[4]`. Most programs that do out of bounds pointer arithmetic are doing so with pointers from malloc/mmap/similar, which might have similar semantics to arrays but are not arrays.
FilPizlonator drops flags in LLVM IR that would have permitted downstream passes to perform UB driven optimizations.
Does this work reliably or did your patches have to fix bugs here? There are LLVM bugs with floating point where backend doesn't properly respect passed attributes during codegen, which violate the behaviors of user level flags. I imagine the same thing exists for UB.
LLVM is engineered to be usable as a backend for type-safe/memory-safe languages. And those flags are engineered to work right for implementing the semantics of those languages, provided that you also do the work to avoid other LLVM pitfalls (and FilPizlonator does that work by inserting aggressive checks).
Of course there could be a bug though. I just haven't encountered this particular kind of bug, and I've tested a lot of software (see https://fil-c.org/programs_that_work)
However, I would be remiss if I didn't question your historical claim, which seems to me a bit too strong:
> Mathematics predates the idea of formal proof by millenia [...] Formal proof only emerged early in the 20th century [...]
You seem to associate the start of "Mathematics" with Euclid, but (as far as I know) he worked at approximately the same time as Aristotle. Aristotle's syllogisms are perhaps the most famous formal logic system: their correctness relates only to their form, not their content. All deductions of the form "All X are Y, All Z are X, hence All Z are Y" are valid (assuming the premises are), regardless of the meanings of X, Y, and Z. (Outside of Greece, my understanding is that a few hundred years earlier Panini had also developed a system of formal manipulations, but for representing grammars.)
What, to my understanding, "emerged" only the 19th and 20th century was 'merely' a formal logic both expressive and sound enough to properly express modern mathematics (the Beggriffsschrift in the 19th century and FOL+ZFC in the 20th). Between Euclid and the 19th century the development of calculus was probably the biggest advance in mathematics, and my understanding is that Leibniz himself spent significant time working on formal logic.
Perhaps I have the wrong definition in mind of 'formal logic' or 'mathematics,' but I do think the history of formal logic is much more closely tied to the history of mathematics than your post makes it seem on first glance. Though I certainly agree that "mainstream mathematics" has never felt it necessary (or necessarily that useful) to express proofs in a formal logic carefully enough that they could be checked by computers; this was a fringe focus of a minority group of mathematicians and computer scientists that was co-opted as a marketing stunt into 'what mathematics is' for major corporations trying to justify their money burn.
reply