Continuous relaxation of boolean algebra is an old idea with much literature. Circuit synthesis is a really well-researched field, with an annual conference and competition [1]. Google won the competition 2 years ago. I wonder if you have tried your learner against the IWLS competition data sets. That would calibrate the performance of your approach. If not, why not?
One of the main use-cases for compile-time metaprogramming (like macros) has been to be able to write performant code that does not type-check correctly in a typed language. Library writers encounter this issue frequently, e.g. the C++ standard library is heavily based on template metaprogramming. One example of code we want to write in a generic way are map and flatMap operations that you can define on lists, binary trees, hashmaps, rose trees and many other container-like data structures. But many typing system do not let you write the map and flatMap abstraction in a type-safe way once and for all. In dynamically typed languages, there is no such issue.
Some modern languages (Haskell, Scala) overcome the lacking expressivity for library writers with higher-kinded types and principled support for ad-hoc polymorphism (e.g. typeclasses), thus reducing the need for meta-programming. Notably, Haskell and Scala have unusually principled support for metaprogramming.
As a heuristic, I would suggest that using metaprogramming for small or medium sized normal ("business") code is a sign that something maybe be suboptimal, and it might be worth considering a different approach (either to the choice of implementing business logic or the chosen programming language.)
I wonder if you vould you point me to concrete examples where people write PTX rather than CUDA? I'm asking because I just learned CUDA since it's so much faster than Python!
For various micro-bench reasons I wanted to use a global clock instead of an SM-local one, and I believe this was needed.
Also note that even CUDA has "lower level"-like operations, e.g. warp primitives. PTX itself is super easy to embed in it like asm.
There isn't a lot of easily accessible examples outside of the corporate world.
Open source authors typically shy away from Nvidia closed source APIs, and PTX is tied to how Nvidia hardware works, so you won't see it implemented for other hardware.
To do what Deepseek did, but didn't want to waste your time and money with Nvidia, you'd use Vulkan. Theres more Vulkan in the world than CUDA.
Category theory is an API for mathematics that was developed with specific applications in mind that the API seeks to unify and make easier to think about. Those application domains are algebraic geometry, algebraic topology, homological/homotopical algebra.
Every API comes with trade-offs: typically an API makes one domain easier, at the cost of making other domains harder. Example: CSS is Turing complete.
And I think CSS is really good at helping with styling webpages. But I would not want to write a compiler is CSS.
Computer scientists, like myself, who read from Page 150
onwards have just found the API stylised for
algebraic geometry, algebraic topology, homological/homotopical
algebra, ... not that useful, for applications in computer science. Unlike the first 50 pages, which have been very useful. More specifically, we found the cost of using purely categorical APIs not worth the benefits in many application domains. Maybe we are missing something, maybe we overlooked something. But, given the investments since the 1990s of computer science into category theory, I'd like to see more evidence for!
To conclude with a concrete example: why would I write a compiler using an API for homotopical algebra?
Rage clicks pay, shallow dismissals are easy to produce -- no
time-consuming investigative journalism necessary.
Most important perhaps is that new media like
Substack are in direct competition with traditional newpapers like the
NYT.
Coase's great insight (in: The Nature of the
Firm, 1937) was that firms exist in order to reap economies of
scale. Traditional newspapers reaped economies of scale from printing,
paper distribution, subscriber and advertiser management. Essentially
all of this is gone. What modern newspaper scale on is branding, and
and selling influence, but this is in direct contradiction with strong
journalists' interest (who do not like to be told by their editors what to write and how). Until recently, top journalists could not go alone, since they lacked the expertise to handle monetisation of their writing. This changed with the likes of Substack, which centralises
(automates) subscriber management, and technical infrastructure, but
without editorship.
Hence, top writers are increasingly moving away from
traditional newspapers to something like Substack, with Greenwald
and Scott Siskind being two high-profile examples. They won't be the
last.
Newspapers see the writing on the wall and fight back.
Things like integrity and trust matter more than ever, so the idea that newspapers would jeopardize that to get back at a somewhat meaningless scoop is pathetic.
The time will soon come when we cannot trust anything we don't see with our own eyes, and we will then need to have a web of trust with reliable sources.
Newspapers can still capitalize on being a source of trust and truth, if they don't fuck it up.
Of course, the NYT is still pretty reliable on citations of fact, even if their slant is worse than it should be.
I don't know, the more I think about it the less sense it makes. I wonder if we can apply Hanlon's Razor[1] and say it was just a poorly researched article. If the author did some brief googling for things people have said about Scott and his blog, they'll find other people who have quoted him out of context. For the example of "feminists are voldemort", Scott did mention that he's been quoted out of context lots of times on that line so it should show up lots of time on the internet. It might have been a sloppy re-quote instead of original research. Maybe it wasn't so much a hit-piece as a reflection of the easy-to-find popular trends of discussion about Scott's writing. In that case the NYT piece was very irresponsible, but not really malicious.
Part of the reason I'm leading this way is because and the end of the day, Scott just doesn't seem important enough to the NYT to focus on for a hit piece. And even then it reads more like a condemnation of SV tech culture than it does as a condemnation of Scott (however unfair it was to him).
Unfortunately, we know for sure that it was not just a poorly researched article. From Scott Aaronson[0]:
> I spent many hours with Cade, taking his calls and emails morning or night, at the playground with my kids or wherever else I was, answering his questions, giving context for his other interviews, suggesting people in the rationalist community for him to talk to…
and
> Was there some better, savvier way for me to help out? For each of the 14 points listed above, were I ever tempted to bang my head and say, “dammit, I wish I’d told Cade X, so his story could’ve reflected that perspective”—well, the truth of the matter is that I did tell him X! It’s just that I don’t get to decide which X’s make the final cut, or which ideological filter they’re passed through first.
I take your point with regard to the economic incentives at play. But at the end of the day, it seems likely that the net effect of this article will be to drive more readers to the new Subspace blog? (A sort of Streisand effect.)
That is likely to be the case. However the performance metrics that the authors are being evaluated on (like clicks, retweets, word-count) are unlikely to include hard-to-measure long-term effects like Streisand.
I think we are seeing a wounded animal's fight for survival ....
It has often been noted that many political concepts in the western world emerged out of Christianity, notably by Nietzsche and Carl Schmitt. That's probably not really directly a unique feature of Christianity but because religions themselves tend to co-evolve with successful states as narratives that help stabilise said states.
That isn't strictly true. Christianity has a concept of what should be dealt by God and what should be dealt with by man. The very term "Religion" is a Christian one as before that generally the state, religion, your life etc were all bound up as one. It wasn't until the Roman Empire did anyone even consider that these were separate.
I recommend a little less parochialism, and more historical scholarship.
All populist politics needs to appeal to its clientele with simplistic, easy to grasp utopias that are claimed to be in easy grasp after "we" win power, whether it's
the classless society of Marxism,
notions of paradise in various religions (e.g. 72 seventy-two houri in Sunni-Islam), libertarianism's coercion-free optimal resource allocation,
anarchism's absence of social hierarchy,
Robespierre's "liberté, égalité, fraternité", and many others.
"Woke" culture is clearly a contemporary evolution (rebranding) of the
socialist tradition emerging out of the French revolution, and made politically potent by Lenin, Stalin & comrades, channeled into the modern western world via Gramsci's cultural hegemony, and nowadays spread by powerful branding organisations like Avaaz [1] and Purpose [2].
Lean. It's implemented in a
dependently typed programming
Lean is implemented in C++ [1, 2]. There's a message in there somewhere. The message is probably something along the lines of: if you want performance, use a low-level language.
I'm aware, I have a branch implementing C FFI for Lean 3; my point was that it's logic, mathlib could be implemented in system F instead. I'm pretty sure Lean could be implemented in Lean eventually.
What do you mean by "it's logic, mathlib could be implemented in system F"? System F is not dependently typed!
Anyway, nobody doubts that Lean's logic is a dependently typed formalism: "Lean is based on a version of
dependent type theory known as the Calculus of Inductive Constructions" [1]. I thought the discussion here was about using dependent types in programming languages. Note that logics and programming languages are not the same things.
[1] J. Avigad, L. de Moura, S. Kong, Theorem Proving in Lean.
That's an interesting question: can Lean be implemented in Lean's dependent type theory.
I'm not currently working with Lean, but I will start a large verification project in a few months. We have not yet decided which prover to go for. We may write our own.
This is misleading. There are two notions of scalability:
- Scalable to large code bases.
- Scalable to deep properties.
Deductive methods are currently the only ones that scale to deep properties. Model checking et al are currently the much better at scaling to large code bases. Note however two things: First, Facebook's infer tool which scales quite well to large code bases, is partly based on deductive methods. Secondly, and most importantly, under the hood in most current approaches, SAT/SMT solvers do much of the heavy lifting. Existing SAT/SMT solvers are invariably based on DPLL, i.e. resolution, i.e. a deductive method.
> Deductive methods are currently the only ones that scale to deep properties.
Model checkers check deep properties with overall significantly less effort. It is true that they don't always succeed, but neither do deductive proofs. In industry, deductive methods are used as a last resort, when they're used at all, to tie together results from automated techniques.
> Note however two things: ...
That's not what I meant by "deductive methods;" I meant verification by semi-automated deductive proofs. Also, SMT solvers aren't used in isolation to verify significant pieces of software, they're used as components of model checkers, concolic testing and proof assistants (or to verify local properties of code units), so they're used in both semi-automated deductive methods as well as in automated methods. I also believe that DPLL is based on assignment and backtracking, not resolution.
DPLL is based on a form of resolution, in real implementations you mostly simply enumerate models, and backtrack (maybe with some learning) if you decided to abandon a specific model.
TLC is a model checker can check most properties expressible in TLA+, which are more expressive than any base lambda-calculus theory (e.g. it includes temporal refinement properties). See my overview on TLA+'s theory: https://pron.github.io/tlaplus
> in real implementations you mostly simply enumerate models, and backtrack (maybe with some learning) if you decided to abandon a specific model
So not deductive. You know that because DPLL does not directly yield a proof of UNSAT.
Lamport's TLA contains ZF set theory. That makes TLA super expressive. Unless a major breakthrough has happened in logic that I have not been informed about, model checkers cannot verify complex TLA properties for large code bases fully autom atically. Let's be quantitative in our two dimensions of scalability:
- Assume we 'measure' the complexity of a property by the number of quantifier alternations in the logical formula.
- Assume we 'measure' the complexity of a program by lines of code.
(Yes, both measures are simplistic.) What is the most complex property that has been established in TLA fully automatically with no hand tweaking etc for more than 50,000 LoCs? And how does that complexity compare to for example the complexity of the formula that has been used in the verification of SeL4?
So not deductive.
So first-order logic is not deductive, because it doesn't yield a direct proof of FALSE?
There is an interesting question here: what is the precise meaning of "deductive"? Informally it means: building proof trees by instantiating axiom and rule scheme. But that is vague. What does that mean exactly? Are modern SAT/SMT solvers doing this? The field of proof complexity thinks of (propositional) proof systems simply as poly-time functions onto propositional tautologies.
> What is the most complex property that has been established in TLA fully automatically with no hand tweaking etc for more than 50,000 LoCs? And how does that complexity compare to for example the complexity of the formula that has been used in the verification of SeL4?
TLC, a model checker for TLA+, is commonly used to verify arbitrary properties -- at least as "deep" as those used in seL4, and often deeper -- of TLA+ specifications of a few thousand lines. Those properties can informally correspond to codebases with hundreds of thousands of lines, but there is currently no method for formally verifying arbitrary properties of 50KLOC, be it automatic or manual. Automated methods, however, are used either for deep properties (quantifier alterations) of few k-lines of spec/code or shallower (though still non-local and non-compositional) properties of 50-100KLOC. Manual deductive methods are virtually used for nothing outside of research projects/teams, except for local, compositional properties, of the kind expressible by simple type systems.
> So first-order logic is not deductive, because it doesn't yield a direct proof of FALSE?
In any logic you can work deductively in the proof theory, or in the model theory. DPLL SAT solvers work in the model theory of first-order logic. Also, SAT solvers work on propositional logic, not first-order logic. Because of completeness, we know that every model-theoretic proof corresponds to a proof-theoretic proof, but that's not how most SAT algorithms work (except for resolution solvers).
> There is an interesting question here: what is the precise meaning of "deductive"?
It means using the syntactic inference rules of a proof theory, rather than the semantic rules of a model theory (possibly relying on completeness meta-theorems, as in the case of propositional logic, although that's not relevant for most interesting first-order theories). SMT solvers employ SAT, and can work on some first-order theories. I am not familiar with all the techniques SMT solvers use, but I believe they employ both proof-theoretic and model-theoretic techniques. In any event, as I mentioned before, SMT solvers are rarely used alone, because they're very limited. They are used as automated helpers for specific steps in proof assistants (TLAPS, the TLA+ proof assistant makes heavy use of SMT solvers for proof steps), for local properties of code (e.g. OpenJML for Java, in Dafny and in SPARK) or as components in CEGAR model checkers and in concolic test systems.
TLC ... is commonly used to ...
at least as "deep" as those
used in seL4, and often deeper
What you are in essence implying here is that the SeL4 verification can be handled fully automatically by TLC. I do not believe that without a demonstration ... and please don't forget to collect your Turing Award!
One problem with model-checking is that you handle loops by replacing loops with approximations (unrolling the loop a few times) and in effect only verifying properties that are not affected by such approximations. In other words extremely shallow properties. (You may use different words, like "timeout" or "unsound technique" but from a logical POV, it's all the same ...)
the model theory ...
rather than the semantic
rules of a model theory
All mathematics is deductive.
ZFC is a deductive theory, HOL is a deductive theory, HoTT is a deductive theory. MLTT is a deductive theory,
Quine's NF is a deductive theory.
With that, what mathematicians call a model is but another deductive theory, e.g. the model theory of Peano Arithmetic happens in ZFC, another deductive theory.
The deductive/non-deductive distinction is really a discussion of different kinds of algorithms. Deduction somehow involves building up proof trees from axioms and rules, using unification. It could be fair to say that concrete DPLL implementations (as opposed to textbook presentations) that are based on model enumeration, non-chronological backtracking, random restarts, clause learning, watched literals etc don't quite fit this algorithmic pattern.
I am not sure exactly how to delineate deductive from non-deductive algorithms, that's why I think it's an interesting question.
SMT solvers are rarely used alone,
I agree, but model checkers, type checkers for dependent types , modern testing technques, and (interactive) provers all tend to off-load at least parts of their work to SAT/SMT solvers which makes the opposition between deductive and non-deductive methods unclear.
* * *
BTW I am not arguing against fuzzing, concolic, model checking testing etc. All I'm saying is that they too have scalability limits, just that the scale involved here is not lines of code.
> What you are in essence implying here is that the SeL4 verification can be handled fully automatically by TLC.
No, I am not. Read what I wrote again :)
> and please don't forget to collect your Turing Award!
Some people have already beat me to it. The 2007 Turing Award was awarded for the invention of model checkers that precisely and soundly check deep properties.
> One problem with model-checking is that you handle loops by replacing loops with approximations
No, that's what sound static analysis with abstract interpretation does. Model checkers are both sound and precise, i.e. they have neither false positives nor false negatives. To the extent they use sound abstraction (i.e. over-approximation), as in CEGAR algorithms, they do so to increase performance and to sometimes be able to handle infinite state spaces. A model checker, however, is always sound and precise, or else it's not a model checker.
> In other words extremely shallow properties.
Model checkers commonly check arbitrarily deep properties. Engineers in industry use them for this purpose every day.
> All mathematics is deductive.
Yes, and all (or much, depending on your favorite philosophy of mathematics) of it has models. If you have two apples in one hand and one apple in the other and you count how many you have, you have not done so using deduction in any logical theory. That had you used such a process you would have also reached the same result is because of soundness and completeness meta-theorems. That mathematics has both proof and model theories, and that they're compatible, is the most important result in formal logic.
> All I'm saying is that they too have scalability limits, just that the scale involved here is not lines of code.
All verification methods are limited by both size of code and depth of properties. For non-trivial property, the least scalable method, on average, is deductive proof. Which is not to say it is not useful when automated methods have failed.
Sorry, I got confused about loops in model checking, I was wrong about that. I don't know what happened, since I even have co-authored a model-checking paper where we do check loops.
Be that as it may, seL4 cannot currently be automatically verified, and it's not due to code size (8700 lines of C and 600 lines
of assembler). It's hard to see what the obstacle to mechanisation could be but logical complexity.
Model theory is not some magical deduction-free paradise. The reason we care about model theory in logic is because we want to have evidence that the deductive system at hand is consistent. Building models of Peano arithmetic in ZFC for example, but also relating constructive and classical logic through double negation or embedding type theory in set theory, are all about relative consistency. It's easy to make a FOM (= foundation of mathematics) unsound, and logical luminaries including Frege, Church and Martin-Lof managed to do so. Those soundness proofs in essence transform a proof of falsity in one system to the other, and relative consistency is the best we can get in order to increase our confidence in a formal system. It is true that traditional model theory, as for example done in [1, 2, 3]. doesn't really foreground the deductive nature of ZFC, it's taken for granted, and reasoning proceeds at a more informal level. If you want to mechanise those proofs, you will have to go back to deduction.
> It's hard to see what the obstacle to mechanisation could be but logical complexity.
There is no impenetrable obstacle if humans could do it (for some definition of "could"), but the difficulty is handling infinite state spaces. Model checkers can do it in some situations, but the could do it in more. Neither model checkers nor humans can handle infinite state spaces -- or even very large ones -- in all situations (halting problem and its generalizations).
> Model theory is not some magical deduction-free paradise.
I just pointed out that some of the most successful automated methods, like model checkers (hence their name, BTW) and SAT solvers (which are really special kinds of model checkers), work in the model, not the proof theory.
> The reason we care about model theory in logic is because we want to have evidence that the deductive system at hand is consistent.
The reason we care about models is that we want to know that the "symbols game" of formal logic corresponds to mathematical objects; i.e. that it is sound -- a stronger property than consistency. The model existed first. Proof theory in deductive systems -- and formal logic in general as we know it -- is a 20th-century invention (well, late 19th but only accepted by mathematicians in the 20th).
[1] https://www.iwls.org/iwls2025/