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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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: -…
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…
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…
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,…
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…
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…
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…
pros/cons The main issue is proof automation. Curry-Howard based provers (Coq, Agda, Lean etc) are nice for teaching but if you want to get work done (e.g. you want to verify an OS kernel), you need to automate as much…
Nobody has credible data enabling reproducible comparison of programming languages. The big lacuna of PL research ... If popularity mattered ... PHP, JavaScript etc. I find the evolution of all successful programming…
Worked out pretty well, I think. Au contraire mon ami! ML was better than most of its successors, including Java, which held programming back. Milner's ML avoided some of Java's glaring mistakes (e.g. exception…
Thanks. We were talking cross-purposes. I was thinking about partially initialized arrays in the context of a Rust-like type-checker. I don't think the analysis you ran in 1981 in a prover is possible in 2020 in a…
partially initialized arrays I agree that partially initialized data structures are important for low-level, performance-oriented programming. But it is not clear how to do this within a Rust-style type-based approach…
Albert Cohen from Google gave a really good lecture on polyhedral compilation in the real world at PLISS [1] this year: slides [2], lecture videos [3, 4]. A core problem of the polyhedral approach, is that the thing…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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: -…
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…
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…
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,…
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…
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…
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…
pros/cons The main issue is proof automation. Curry-Howard based provers (Coq, Agda, Lean etc) are nice for teaching but if you want to get work done (e.g. you want to verify an OS kernel), you need to automate as much…
Nobody has credible data enabling reproducible comparison of programming languages. The big lacuna of PL research ... If popularity mattered ... PHP, JavaScript etc. I find the evolution of all successful programming…
Worked out pretty well, I think. Au contraire mon ami! ML was better than most of its successors, including Java, which held programming back. Milner's ML avoided some of Java's glaring mistakes (e.g. exception…
Thanks. We were talking cross-purposes. I was thinking about partially initialized arrays in the context of a Rust-like type-checker. I don't think the analysis you ran in 1981 in a prover is possible in 2020 in a…
partially initialized arrays I agree that partially initialized data structures are important for low-level, performance-oriented programming. But it is not clear how to do this within a Rust-style type-based approach…
Albert Cohen from Google gave a really good lecture on polyhedral compilation in the real world at PLISS [1] this year: slides [2], lecture videos [3, 4]. A core problem of the polyhedral approach, is that the thing…