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…
> 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!
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…
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…
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…
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…
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…
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…
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…
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: -…
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,…
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…
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…
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…
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…
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…
> 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!
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…
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…
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…
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…
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…
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…
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…
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: -…
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,…
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…
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…
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…
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…