MZan @mzan@qoto.org

@loke I'm not a mathematicians, but I will underline two things.

First, in a formal proof you had to prove that all the initial conditions C1..Cn can be respected. Often this is implicit. Then you introduce the assumption P that you want to disprove. So, if P causes a contradiction, but C1...Cn can be respected, it is P that is impossible to respect, given C1...Cn. Usually C1...Cn are not strong conditions, but rather generic conditions. So often there is no explicit proof about the fact that they can be respected. Often it is true by construction.

Second: not all "proof by contradiction" are strictly "by contradiction", but many of them are simpler cases of "refutation by contradiction" and they are accepted also in intuitionistic logic.

A "refutation by contradiction" is based on this: C1...Cn are initial conditions that can be respected; I suspect that P is not respectable, i.e. that "not P" is true; I assume P and I show that P cannot be respected.

The integer between 0 and 1 is an example of "refutation by contradiction". I suspect that there is no such number; I assume it exists; I obtain a contradiction.

Instead a "proof by contradiction" using the rule of the excluded middle, is less direct, because we assume that if "not P" introduces a contradiction, then "P" must be true, but in the proof we have no directly proved the existence of P. These proofs are not accepted by intuitionistic logic.

@hayley reading this book is a cure for who suffers of Impostor Syndrome.

@Lana I bet that feminists will be offended if Macron will use the "Master Chef Last Supper" image during an institutional event about "The professional cooking day" because they are nearly all men. Or someone can be offended if during the "Father Day", Macron displays the Homer Last Supper". The "Lost" image will be not very accepted, if used during the inauguration of a new airport. Context is important.

@ambulocetus I agree with @freemo: SmarterEveryDay is not spreading misinformation. In no part of the video, he lied.

The suggested book is controversial, but he warns about this, and he specifies that it is mainly a philosophical book, to read with open-mind. So, he is fair.

IMHO, the misunderstatement is here: he compares the sense of wonder observing the flagella in the small, to the sense of wonder observing the Universe in the large (and this is fair); science cannot explain why the Universe and/or its laws exist; because science cannot explain all, philosophical reflections are legitimate; he miss to underline that science can explain how flagella evolved and there is consensus about this.

He should be more precise/pedantic in the last point, but the focus on the last part of the video was about the wonder of Universe and life, and not anymore about scientific truth, so *if* it is an error, it is an error made in good faith.

@alexraffa stavo curiosando in giro... su computer di amici/parenti dove avevo messo OpenSUSE Leap ho visto (almeno in passato) diversi delta RPM.

Invece su OpenSUSE Tumbleweed solo RPM normali.

Avrebbe senso usarli anche su OpenSUSE Slowroll, dato che di solito qua uno installa tutto in modo "cronologico" come con Leap.

@toad

@samim to be fair I like political content, but the sad truth is that now-days it is usually associated to propaganda, repeated slogans, cheering, etc...

In this form it is for sure "toxic shit", because it is an useless battle between people speaking, but not listening.

In real life and with Mastodon toots, it is nearly impossible to change the political idea of other people. But, at the same time, it should be nice to exchange different point of views, and/or reporting some fact, without the claim to change other people mind.

But now-days, if you are sincere, you risk to be labelled and cancelled. There can be a grain of truth in every different political idea, but politicians like irrational extremism: if you don't think exactly like me, you are an enemy. So they can spend in campaign and slogans, but less in real actions 🙂

@nobodyinperson section 13 of AGPL says that if users can interact with a modified version of an AGPL program, then you had to distribuite under AGPL also the modified code.

But then we must define "modified version of a (A)GPL program"...

Using git-anex inside a shell script or a bigger service, is usually freely permitted, because it is covered by " This License explicitly affirms your unlimited permission to run the unmodified Program.".

But if the shell script or the bigger service is adding more functionanilities to git-anex, that should be considered as part of git-anex? Are you still an user of git-anex program/service, or are you extending it, circumventing the (A)GPL? Problably only a judge can decide this.

Usually if you are using git-anex like a service, then you can use it freely, and the larger service is not obliged to be under AGPL, because you are only an user of git-anex. Every time you improve git-anex, for working better inside your larger service, then you had to release only these improvements to git-anex, under AGPL.

But the line between using a service, and extending it, can be blur in some cases.

Note that in some cases, you can also produce a larger service, compiling git-anex code inside your "aggregate code", without the need to relaese the full "aggregate code" under (A)GPL. It is in the final part of section 5, but these definitions are not so much clear, IMHO.

@hayley @larsbrinkhoff Clojure is a PoW Lisp, while Common Lisp is a PoS. CL code is forever.

@hayley ah, I found recently this #commonlisp DSL https://nikodemus.github.io/screamer/ and it supports both global compilation and interactive programming. It is doing many tricks: it redefines "defun"; it performs a code-walk on the entire loaded package; it maintains a data-structure at run-time with Screamer-compiled/managed functions and their dependencies, and so on.

@hayley after you read enough posts, you didn't notice anymore rants about the Lisp parens. They just disappear :-)

@jcastp @daviwil Thinking on this, probably it is reasonable mastering Emacs Lisp only if the majority of work and workflow is done inside Emacs (e.g. shell commands, DBMS administration, document search, email and so on). In this case, one can integrate and automatize various parts of his workflow. The Emacs experience will improve to a level unmatched to many other environments like GNOME/KDE and probably also the Web.

For the rest, Emacs is so powerful and rich of extensions, that one can spend years discovering new tricks, without the needing to write a line of Lisp, except configurations. So, for normal usage, I think that Emacs Lisp is not necessary at all.

@hayley yes, I agree. Obviously my "without the needing to add other things" was a partial hype.

JVM now supports virtual-threads, but in CL threads are a de-facto standard and there are also DSL in CL for green/cooperative-threads and maybe it is not so hard to add something at the compiler implementation level.

Global user-specified optimizations are outside the scope of CL macro, because they can walk only local code. But you can put all the DSL inside a grouping macro, like Coalton is doing. In this way you can abuse the macros, but you can support more declarative DSL, needing a lot of analysis, and not only "stupid" code expansion.

C-like global optimizations can be supported from CL compilers, if one has a way to tell which parts of the implementation is sealed. CLOS has already an API for this, IIRC. Some commercial compilers are already doing this on normal CL code, IIRC.

OCaml added recently a very complete and powerful effect system, well integrated in the language. But the venerable conditions system of CL is good enough in a lot of cases, and still years ahead respect other mainstream PL.

@hayley

regarding this https://erights.medium.com/the-tragedy-of-the-common-lisp-why-large-languages-explode-4e83096239b9 to be fair, C++ is a large and complex language but it keeps growing. Also Java has new features, and/or more dialects like Kotlin.

Common Lisp can grow as libraries, DSL and macros (because it is an extensible language), but its specification is stable and immutable. It is a mature and usable language, without the needing to add other things.

@calebdenman

"A photo is worth a thousand lies" -- CIA

@NanoRaptor

@cmconseils

We need to be realistic. In November, 48% will win Trump, 44% will win Biden, 8% UFO will reveal us that we are on Candid Camera!

@m3tti because it is fun to use. It is the most interactive of all Lisp. You can test immediately functions. In case of errors, you can see the stack, with the values passed to the functions. These values are fully inspectable: you can navigate in structures and objects and so on.

The effect is that you can easily enter into the zone, and play with your code.

#commonlisp is also an extremely rich language, full of features.