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.
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 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.
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).
Compositionality is paramount and category theory guarantees compositionality, but the author's criteria for what entails a good configuration language are woefully naïve.
Configuration is not about describing data, it's about control. Control over a system made of impure, effectful parts.
Configuration is a matter or programming a mutable computer, i.e. a way to specify the composition of effects that you want.
The configuration language is agnostic over the systems it controls, therefore it must provide semantics that preserve morphism in any of its interpetations. The language must be rich enough to accomodate for this. It is not enough to have one semantics.
Moreover, it must be rich enough to describe its own models. Yes, the interpretation of it by arbitrary systems must be expressible in the language itself in order to be meaningful and to preserve consistency with regard of its interpretations. In practice, this is done through types.
Additionally, configuration is a global activity, it's applied to the whole system, with many people changing conflicting aspects of it. Just like with any large evolving program, abstraction and typing are required for software engineering reasons alone.
Coincidentally, CUE is also a monoid, but it is more than that, it is a complete Heyting algebra (or a complete Boolean algebra in the case of closed world assumption), these objects also form very rich categories.
Another way to look at CUE is to view it as a semantic domain for the denotation of arbitrary types of arbitrary languages. It's suitable for this because it's a coherence space (Girard). All CUE operations are closed, preserving the structure of the space.
One interesting aspect of author's effort is that even if he was so naïve, category theory led him to a path that is correct. What he did is incomplete, a monoid does not suffice for a configuration language, but a monoid is required. This is saying something.
No, we do have a spec[1], but it cannot be as concise as the JSON link posted because the JSON link is mostly only about syntax, and our spec discusses both syntax and semantics. And of course, we are a much richer language than JSON, with many more features and computational behavior.
That being said, it would be nice to use railroad diagrams to describe syntax in our spec.
Among types and other useful properties, CUE supports everything you asked for. We're even considering adding a "data-only" mode to CUE which would be exactly what you asked for.
> The original Etak units always had the map oriented with north at the top. That was the way sailors used maps. Honey said they'd discovered that about 20% of the population could not cope with a map that wasn't aligned with the direction they were going, which is why they started rotating the map based on vehicle travel.
I am the opposite, I cannot deal with a map that does not have north on top and it's constantly moving. Modern mapping software sometimes makes it frustratingly hard to keep north on top.
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.