Viewing profile — 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]. Go…

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

> 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 muc…

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 abou…

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 l…

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 direc…

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 probabl…

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 u…

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 loop…

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 …

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…

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 n…

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

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 formal…

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…

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 cur…

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 …

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 invent…

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 to…

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…

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 per…