Cladode

10 ms·

1.
by Cladode 2y ago
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 t
2.
by Cladode 2y ago
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++ stan
3.
by Cladode 2y ago
> 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!
4.
by Cladode 2y ago
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, a
5.
by Cladode 6y ago
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 wou
6.
by Cladode 6y ago
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. Co
7.
by Cladode 7y ago
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 Chr
8.
by Cladode 7y ago
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 af
9.
by Cladode 7y ago
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 automati
10.
by Cladode 7y ago
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 be
11.
by Cladode 7y ago
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.
12.
by Cladode 7y ago
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.
13.
by Cladode 7y ago
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 ca
14.
by Cladode 7y ago
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 learnin
15.
by Cladode 7y ago
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
16.
by Cladode 7y ago
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 versi
17.
by Cladode 7y ago
remove the barrier between types and terms then ... ... you will loose type inference, and hence Haskell becomes completely unusable in industrial practise.
18.
by Cladode 7y ago
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
19.
by Cladode 7y ago
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 prope
20.
by Cladode 7y ago
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 logi
21.
by Cladode 7y ago
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 th
22.
by Cladode 7y ago
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
23.
by Cladode 7y ago
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, f
24.
by Cladode 7y ago
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 o
25.
by Cladode 7y ago
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
26.
by Cladode 7y ago
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 min
27.
by Cladode 7y ago
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
28.
by Cladode 7y ago
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.
29.
by Cladode 7y ago
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
30.
by Cladode 7y ago
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 ex

More ›