Cladode

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?

[1] https://www.iwls.org/iwls2025/

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.)

> write their stuff in PTX

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!

But why is that a problem?

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?

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 ....

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.

   replaced Christian with

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.

   woke/Fox News Cult.

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].

[1] https://en.wikipedia.org/wiki/Avaaz

[2] https://en.wikipedia.org/wiki/David_Madden_(entrepreneur)

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.

[1] W. Hodges, Model Theory.

[2] D. Marker, Model Theory: An Introduction.

[3] C. C. Chang, H. J. Keisler Model theory.

   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.

   In software verification, 
   a sound technique is ...

In other words, tests are not sound ... Anyway, we are quibbling about meaning of words, so this is unlikely to be fruitful.

Tests are not sound in the sense of conventional program logic (overapproximation). O'Hearn's [1] even proves a soundness theorem. So when you say say [1] is not sound then this is confusing for the reader.

   can check most properties 
   expressible in TLA+

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.

   Model checkers check deep 

Which deep properties have you got in mind?

   DPLL is based

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.

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.

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.

    remove the barrier between 
    types and terms then ...

... you will loose type inference, and hence Haskell becomes completely unusable in industrial practise.

   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.

[1] https://github.com/leanprover/lean/tree/master/src

[2] https://github.com/leanprover/lean4/tree/master/src

   better scalability than 
   deductive

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.

This comment is deeply misleading. O'Hearn's incorrectness logic that you cite in your [1] is perfectly sound. It just changes the meaning of Hoare triples from over-approximation to under-approximation. In brief:

- Hoare logic soundly over-approximates

- Incorrectness logic soundly under-approximates

Sound under-approximation is extremely useful when you want to prove that a certain problem must arise in code, rather than may arise. The problem with logic based program verification has often been that your prover could not prove that a program was correct, but, due to over-approximation of traditional Hoare logic, the best you could learn from this failure was (simplifying a great deal) that something may go wrong. That is not particularly useful in practise, since often this is a false alert.

Yes, Miranda was very expensive, had an onerous license and only ran on Unix, that's why researchers felt the need to create a free and open alternative.

Lazy evaluation was invented multiple times. First in theoretical studies of the lambda calculus by Wadsworth in 1971. Later, Friedman & Wise, and independently Henderson & Morris proposd a lazy Lisp, Turner (who later did Miranda) gave SASL a lazy semantics (SASL was eager initially). All three were from 1976, so it was clearly an idea in-the-air. SASL later evolved in to Miranda. Another of Miranda's innovations was to use combinators for graph reduction to implement the Miranda run-time.

Lisp is from the 1950s, dynamically typed and one of the most influential languages of all times. Lisp introduced GC, the single biggest advance in programming languages (but it took 30 years to make it fast). I am not trying to argue that dynamically typed languages became popular in the 1990s.

If anything, I see ML as the (spectacularly) successful attempt at typing Lisp for increasing reliability. Remember Milner was at Stanford in the 1960s, surely he will have conversed with McCarty. Milner's early theorem provers were in Lisp. He invented ML to reduce the pain of using Lisp (remember, ML stands for "meta language"), and to make theorem proving less error prone. More precisely to reduce the TBC (= trusted computing base) in theorem provers through types (viz the famous Thm abstraction).

ML was essentially finished in the late 1980s [1]. Every responsible programming language designer could have taken on board ML's lessons sincen, and it's an interesting historical question why this did not happen.

[1] R. Milner, M. Tofte, R. Harper, The Definition of Standard ML. http://www.lfcs.inf.ed.ac.uk/reports/88/ECS-LFCS-88-62/

   before 2000.

In fairness, the adoption of typed languages in the 1990s was about C/C++, Java, possibly Pascal, Delphi, Ada. None of those languages were built upon ML's innovations (type inference, first-class generics, first class higher-order functions, pattern matching etc). I conjecture that the rise of dynamically typed languages was primarily because the aforementioned typed languages adopted an awkward approach to typing (no inference, subtyping + casting to implement both, ad-hoc polymorphism and generics, or, in the case of C++, generics by compile-time meta-programming which has been awkward in other ways).

So 1990s types were a worst-case scenario: not expressive enough for many practical cases (you had to cast a lot anyway), hence the safety you get from typing was not much, syntactically heavyweight, bad error messages. Pointless trivial type annotations like

   A a = new A(...);

are truly grating, but ubiquitous in the typed languages popular in the 1990s. No wonder people preferred Python ...

We've discussed this before [1], but what I've called the ML-ification of programming languages (static types, type inference, higher order functions, exceptions, ...) has been pervasive. Your own Java has been doing quite a bit of this recently. All major software companies (FB, GOOG, MS) have by now retrofitted types to their dynamically typed legacy languages. Even smaller outfits that are based on dynamically typed legacy languages (e.g. Strip, Dropbox) are retro-fitting typing.

[1] https://news.ycombinator.com/item?id=22068223

I'm still unclear about this, should this be done by the typing system or by an external static verifier:

   simple inductive proofs to show 
   that as you initialize 
   another element and add 1 to 
   the counter

If the latter, you can already do this with Rust as it is, it's just a question of building such a static verifier. If the former, I really doubt that this can fit in Rust's typing system without major surgery. We know well how to add arithmetic to typing systems, but the natural approach to doing so (dependent types) will probably make type-checking / -inference undecidable.

    there are things that you either 
    can't express, or are very hard
    to express, in safe Rust.

This is true (and in some sense inevitable by Rice's theorem) but it is unclear what can be done about this. Bear in mind that Rust's design constraints are

- decidable (indeed fast) type-inference/type-checking

- simple typing system

- you don't pay for features you don't use

It is easy to get rid of unsafe blocks if you throw complexity at Rust, e.g. use dependent types and / or theorem provers, but all the obvious ways of doing this immediately violate the constraints above. Doing it within Rust's constraints is an open research problem.

   potentially fixable.

What would you use as an objective, measurable criterion that we can use to decided whether a purposed fix is in fact a fix? If you have a concrete design proposal that works (in particular w/o destroying Rust's fast (bidirectional) type-inference/type-checking and the simplicity of Rust's types), and evidence that it's widely applicable (i.e. doesn't just allow to type some trivial edge cases of back-links and partially initialised arrays) that would easily publishable in top PL conferences (e.g. POPL) and a working prototype would help towards getting this into Rust.

I would be happy to help with implementing & writing up such work. I have quite a bit of experience with sub-structural types a la Rust. I have spend some time thinking about this problem space, but didn't manage to crack it. I have an incoming PhD student whom I could ask to help with this.

Yes, Coq has a tactics language. So does Isabelle. What I have in mind are primarily "Hammers", i.e. hooking in fully automatic theorem prover (e.g. MizAR for Mizar, Sledgehammer for Isabelle/HOL, HOL(y)Hammer for HOL Light and HOL4). As far as I'm aware, CoqHammer for Coq is work-in-progress and does not yet provide the level of automation that you get from Sledgehammer in Isabelle/HOL for years. But admittedly, it's been 4-5 years since I last used Coq. At the time, two core issues were the following:

- Existing automatic theorem provers often produced non-constructive proofs.

- Existing automatic theorem provers are mostly for FOL, so the gap to the much more powerful logics of Curry-Howard based provers is bigger than with weaker systems.

Have both problems been solved comprehensively as of January 2020?

I know. There have been a lot of impressive verification work in Coq. Huawei is using Coq to do OS verification. Having less automation to hand, in comparison with Isabelle/HOL makes this a bit harder.

I understand the network effect, I understand that most decisions on PL are not based on technical reasons. Most non-experts mostly worry about syntax, as per P Wadler:

   "The simplest thing to do is a significant 
   change to the semantics. People won't argue 
   the way they do about syntax."

ML had GC, it would have been easy to add dynamic linking, and X Leroy made Ocaml fast, with a tiny fraction of the resources that have been poured into the JVM. Admittedly, this was a major breakthrough that was unexpected. I reckon the main problem was getting OO to work properly with generics: type inference becomes a problem and you have to worry about co/contravariance.

A Hejlsberg certainly wasn't on the ML train in the past. For a start he didn't think generics are a good idea (he told me personaly). Typescript shows that he changed his mind! Go explicitly rejected generics at the start, but Go-2 is scheduled to get them.

Module systems are not such a big deal in my exerience, I don't think ML's was a full success.

That's a subtle and deep question. One example are nominal techniques. Consider Nominal Isabelle. It is known that nominal techniques are contructive. However, when adding nominal techniques to a classical logic, it is natural to express some of this using double negation, leading to only a small blowup in formula size. Existing proof automation can easily handle this blowuip. Doing the same in a simple minded constructive way, leads to a massive formula size increase, defeating (at the time) existing proof automation.

This was a while back, maybe the problem has been solved now, I have not followed this field. But as far as I'm aware, the 'hammering' approach to proof automation that has been working well with Isabelle/HOL has been successfully ported to Coq/Agda etc.