4ad

> Austria is quite far ahead

Yeah, quite ahead in terms of making anonymous phone numbers illegal and requiring the government to know your phone number.

And if you don't want to use a smartphone, ID Austria does not work with regular FIDO security keys, you need special ones. Same for the old SmartCard system which didn't work without government-mandated malware.

It also makes you sound like a conspiracy theory nutjob, and the current political climate in Europe is such that people are really sensitive to this sort of alarmist messaging (which they erroneously perceive as fascist rhetoric) and will not listen to you because they don't want to be associated with those people.

I don't think we can win this fight. Personally I tried to advocate against eIDAS in Austria and I've had negative success. After my warnings, people like it more.

"Oh, it's an EU thing? it must be good!".

Yes, that's true. And there are various logical systems which hint at mutability (apart from linear logic itself). I already mentioned how we can find shared-memory futures in semi-axiomatic sequent calculus. Those futures are mutable, but write-once. This write-once aspect induces a degenerate monotonicity property which can be generalized to arbitrary monotonicity. Mutable variables can exhibit a form of CH as long as writes to them are monotonic in a certain sense, in particular new writes must not refute old reads. For example logical variables in a logic languages are exactly this. Safe, shareable mutable variables which denote evolving proof state during proof search.

They are very different books. TAPL is a book about programming language semantics, TTAFP is a programmer-oriented book about Martin-Löf type theory.

There is very little overlap.

TAPL is definitely the book to pick up if you are interested in programming language semantics. But if you are interested in logic, dependent types, Curry-Howard correspondence there are potentially better and more modern materials than TTAFP (not to say that TTAFP is bad). If you care about formalizing programs Sofware Foundations is a much better resource, and if you care about mathematics and logic, there are resources specifically suited to that.

It's very simple, it's because pure, typed functional programming is not arbitrary but rather fundamental. Natural deduction from logic corresponds to various typed lambda calculi, and functional programming is but a practical manifestation of lambda-calculus.

Under Curry-Howard correspondence simply typed lambda calculus is the term calculus for intuitionistic propositional logic. System F (polymorphic lambda calculus) corresponds to impredicative second-order propositional logic. System Fω corresponds to a kind of higher-order logic. Dependent types correspond to intuitionistic predicate logic, etc.

Other correspondences that are based on sequent calculus instead of natural deduction are more exotic, for example classical logic corresponds to μ~μ-calculus, a calculus of continuations which (very) roughly can be understood as continuation-passing style (but in a principled and careful way). Classical linear logic corresponds to a form of session-typed process calculus. Intuitionistic linear logic corresponds to either a process calculus or to a lambda calculus that is using futures (which can be though as mutable shared memory concurrency using write-once cells).

Note however that languages corresponding to sequent calculus, especially ones that come from a dual calculus (classical logic or classical linear logic) contain some sort of commands, choices that you request from a value, which more or less makes them object-oriented languages, albeit without imperative, mutable assignment. In some sense you can escape functional programming by moving to a dual calculus, but you can't escape purity as long as you care about having propositions as types.

From a Curry-Howard point of view no logic corresponds to a general imperative calculus. Imperative programming is simply not fundamental and generally undesirable when doing logic (so when doing type theory). Mutable state with imperative updates can easily be encoded into FP when needed, e.g. via monads, by using linear types, or by having algebraic effects.

That doesn't mean that types are not useful to imperative languages, of course they are. But types in imperative programming are very weak and logically not very interesting however useful they might be for engineering purposes. Also note that type theory does not mean type system. Many languages have type systems, some more ad-hoc than others, but type theories are special, very specific mathematical objects that embody logic (under the Curry-Howard correspondence). All programs written in a type theory terminate, and this is fundamental. Usual programs, which are not concerned with mathematical proofs certainly don't always terminate.

Of course understanding type theory is a very good way of producing (weaker) type systems that are useful in practical programming, including imperative programming (see for example Rust, which does not employ an ad-hoc type system). Occasionally new logic correspondences are discovered which illuminate certain language features of existing languages. For example Rust's borrowing system was thought to be ad hoc, but now we understand that shared borrows correspond to a logic that arises from semi-axiomatic sequent calculus. The cuts that remain after evaluation (normalization), called snips, are precisely shared borrows, while general cut is memory allocation.

The book in the link is a book about Martin-Löf type theory, which means it is a book about a certain kind of lambda calculus by necessity, there is no other choice.

I don't play video games but I invert the trackpad scroll direction on macOS. I cannot understand people who use the default "natural" scrolling, it's anything but natural, and it's baffling that it's the default.

It would also be a useless article. It's fine to write for an audience, if you're not in the target audience, move on.

It appears that Bear does not accept contributions[1] and the very few contributors it had in the past only contributed a trivial amount of code[2].

But you're right, relicensing requires the approval of all copyright holders, and in general there can be many. Of course many projects require the prospecting contributor sign a CLA where they relinquish their rights to the project in order to be able to contribute. Personally while I have signed some CLAs, such as the Go one where I retained my rights, I'd never sign one which required me to give away my copyright rights, precisely so they wouldn't be able to do a rugpull on me.

I believe that copyright law is the biggest weapon one has against open source rugpulls and one should not give it away.

[1] https://github.com/HermanMartinus/bearblog/blob/master/CONTR...

[2] https://github.com/HermanMartinus/bearblog/graphs/contributo...

The copyright holder (the author) is solely responsible for choosing how they want their work to be distributed, and is not bound by any other sort of constraint. They can choose any license at any time, and change their mind however often, and it whatever direction they want. Any previous licenses used (MIT here) bear no effect whatsoever. There is no license in the world (and cannot be) that would prohibit the copyright owner from changing it. It makes no sense, the license terms only apply to the licensee, not to the licensor.

Of course, the author cannot retroactively change the license of any previously distributed work. Anyone is free to fork off Bear from its last MIT code and do whatever they want with it.

So no, the MIT license does not "explicitly allow to relicense a project at any point" (emphasis mine). The MIT license allows licensees to license their derived work however they see fit, it has no effect on the relicensing by the licensor (the copyright holder).

> While scientists have considered accessing the liquid to further analyze the content, as of 2024, the bottle has remained unopened because of concerns about how the liquid would react when exposed to air.

...This seems like a trivial non-concern? Just open it in an inert atmosphere?

> While it has reportedly lost its ethanol content

Why, and more importantly how would it lose its ethanol content?

I have 40k. Works fine.

Did you disable Memory[1]?

[1] https://help.openai.com/en/articles/8590148-memory-faq

I call BS on that, as Macbooks somehow always kept being 16:10. In fact you could easily buy 16:10 panels, I know because for many years I upgraded old 16:10 Thinkpads with modern displays.

Never used Pocket, but I moved to Raindrop.io (from Pinboard) for my bookmarks. I believe it can import Pocket.

It's hard to say who will fare best, but it's evident who'll do the worst. The European Union will regulate AGI out of existence. Most citizens would not want to use it because of climate change, or something.

I think poor countries with weak democracies or dysfunctional systems would do pretty good with AGI. I don't believe democracy will survive AGI, except, perhaps in the United States.

Learning category theory to the level of understanding monads should take half an hour at most, and would constitute real understanding of what a monad is, versus this C++ explanation which is handwavy even in terms of C++. C++ can't even encode monads accurately!

But one doesn't even need to learn category theory. I assume that everybody has learned abstract algebra in high school, monoid, rings, groups, vector spaces and all that. A monad is just another kind of a structure like that. If you have studied abstract algebra in school then it should take 5 seconds to read the definition of a monad, a minute to understand it, and perhaps 10 minutes to see how various things such as errors or lists form monads.

Learning category theory, or indeed any sort of math from Wikipedia is an absolute futile endeavour.

So you think that a monad which is an object with a simple definition in category theory is better explained in terms of C++?

I would agree that most of these articles about monads are bad. Just study the definition, then study what you can do with monads, it's not that hard.

Great article, two minor nitpicks:

> To avoid Russell's Paradox, there isn't a type of all types. Instead, we have universes.

This is an oversimplification, and Lean-specific (to be fair, the author claims to explore these concept in Lean). Girard's paradox comes from unrestricted impredicativity. To maintain consistency one needs to control impredicativity, type universes are a possible, very straightforward choice, but it is not the only choice.

Some theorem provers, such as Cedille, do not use type universes, and even have `Type : Type` while still being consistent. See Stump, Aaron: “The Calculus of Dependent Lambda Eliminations.” Journal of Functional Programming 27 (2017): e14. DOI:10.1017/S0956796817000053[0]

Additionally:

> The famous Curry-Howard correspondence states [...] Propositions are types in Prop [...]

Curry-Howard doesn't say anything about Prop, Prop vs. Type is just a distinction done in some particular type theories for pragmatic reasons, or because it simplifies classical (as opposed to intuitionistic) reasoning. In fact the reason why Prop vs. Type is a distinction done by many theorem provers leads Lawrence Paulson[1] to claim that modern theorem provers don't really use Curry-Howard[2], at least as Curry-Howard was originally defined. I disagree, because elements of Prop are still types, but please understand that this is a departure from original Curry-Howard.

Moreover:

> The famous Curry-Howard correspondence states [...] True propositions have exactly one term [...]

As explained above, this is not the case for the "original" Curry-Howard, and it is just a choice in Lean, which is a type theory with proof irrelevance. There are different type theories without proof irrelevance (such as Adga by default without a recent extension), and Curry-Howard certainly still applies to them. In fact even in Rocq (Coq), which still has Prop vs. Set, proof irrelevance has to be assumed explicitly[3]. (Rocq also has SProp[4] for proof irrelevant propositions.

nLab has more information about propositions as types[5] vs. propositions as some types[6].

[0] https://doi.org/10.1017/S0956796817000053

[1] https://www.cl.cam.ac.uk/~lp15/

[2] https://lawrencecpaulson.github.io/2023/08/23/Propositions_a...

[3] https://github.com/rocq-prover/rocq/wiki/The-Logic-of-Coq#wh...

[4] https://rocq-prover.org/doc/V8.15.0/refman/addendum/sprop.ht...

[5] https://ncatlab.org/nlab/show/propositions+as+types

[6] https://ncatlab.org/nlab/show/propositions+as+some+types

HDR is about, well, high dynamic range images, usually expressed with at least 10 bits of precision (although it can also be float, etc), and often, but not always encoding scene-referred data instead of image-referred data (originally it was supposed to only encode scene-referred data, but then other competing formats ignored that). It has nothing to do with the gamut and with the color primaries, although in practice HDR images use a large color space.

But you can absolutely have an SDR image encoded using a large color space. So I am not sure why the author talks about color primaries when it tries to justify HDR… I still don’t know what kind of HDR images this new PNG variant can encode.

> This post is mostly AI generated, of course with significant guidance, feedback, iteration and some edits from me.

I can tell, because it is garbage.

AI's notion of PK is useless because of Blum's speedup theorem. Because the invariance theorem fails in PR (PR is not universal), description-length gaps between PR and Turing complete languages can grow without bound.

Essentially a more expressive formalism can encode an interpreter for the weaker one and then diagonalise over it. Restricting yourself to a total language, you sacrifice potentially unbounded conciseness.

This is a profound difference between TC and non-TC languages, and it manifests even for terminating functions. It's not just that a TC languages can encode non-terminating computations, it's that a TC language can encode terminating functions more efficiently than a non-TC language. A terminating program expressed in a total language must manifest its termination proof in a strict way with finite degrees of freedom, whatever the choice of total language might be. In a TC language it doesn't have this artificial constraint.

In some sense, as program complexity grows (expressed in a total language), more and more of the program is dedicated just to encoding its own termination proof. We can sort of see this a corollary of this experimentally with programs (proofs) written in theorem provers like Coq (which are total). Giant proofs extract to very small programs. We don't see the sort of phenomenon in theorem provers using a Curry-style type system, for example Nuprl, where the underlying lambda calculus is Turing complete. This is experimental evidence that even though most interesting functions might be PR, a PR language might not be the best language to express those functions. And this seems to be the case even without choosing specially-crafted pathological examples.

These are subtle issues and I can't fault the author for not knowing about them, but I can fault him for using AI to appear to say something profound when all that was said was woefully naïve.

I want the opposite, an extension that will redirect all crappy frontends to the canonical sources (which work better and I am logged-into, I can comment, etc).

Indeed, KDE is like Windows, which is sad, because I don't like the desktop metaphor, yet KDE is the only group that is concerned with usability and improves the system with every release.

I actually don't mind the GNOME metaphor... but they make it less and less usable over each release. Philosophically, what they are talking about sounds great, but pragmatically the system is just getting less and less usable. UX consistency is good, but not when it comes at the expense of functionality. Also, I don't like that GNOME has been ideologically captured by the extreme left.

Back in the day I ran WindowMaker and FVWM, but nowadays, with Wayland, HiDPI screens and expectations of integration, it is not a viable strategy anymore.

Unless you use a language designed for formal verification (Lean/Idris/Agda/F*/ATS/etc), no, it is not possible.

You can get pretty far in Haskell (with various extensions) and Scala. But for Go/TypeScript/etc, forget about it.

Comparison with TLA+ doesn't make any sense as TLA+ implements a very different sort of logic, but the property that it is a real programming language is shared by virtually everything in this space.

Lean/Adga are real programming languages, while Coq (Rocq), F*, ATS, Isabelle/HOL all extract to various other programming languages.

Frankly, it's TLA+ that is the odd one here.

Dafny is great, and has some advantages compared to its competitors, but unequivocally calling it "the best" is quite bullish. For example, languages using dependent types (F*, ATS, Coq/Adga/Lean) are more expressive. And there are very mature systems using HOL.

Truth is that everything involves a tradeoff, and some systems are better than others at different things. Dafny explores a particular design space. Hoare-style invariants are easier to use than dependent types (as long as your SMT solver is happy, anyway) but F* also has that, except that in F* you can also use dependent types when automatic refinement proofs become inadequate. And F* and ATS can target low-level, more so than Dafny.

Probably I would not use ATS for anything, but between F* and Dafny, there isn't such a clear cut (I'd most likely use F*).

And if I don't need (relatively) low-level, I wouldn't use either.

It not only prevents innovation, but it also enables fake industries, such as companies that harass and "fine" you (not legally binding) for not having an imprint even when not required, or otherwise coming up with irrelevant "problems" with your imprint and reporting you to authorities.

Code bounties are unethical. I will absolutely die on this hill. You benefit from everyone's work, yet only one (or a select few) maybe get paid (in this case a pitiful amount, considering the required expertise).

Almost universally, people attempting a bounty are in a dire financial situation. You’re just taking advantage of them.

No. HDR can encode high dynamic range because (typically) it uses floating point encoding.

From a technical point of view, HDR is just a set of standards and formats for encoding absolute-luminance scene-referred images and video, along with a set of standards for reproduction.