Forwarded from Symptoms
For a long time we have looked for the unity characteristic of the concept of a science in the direction of its object. The object would dictate the method used for the study of its properties. But this was, at bottom, to limit science to the investigation of a fact, to the exploration of a domain. When it became clear that every science more or less gives itself its fact and appropriates for itself, in this way, what one calls its “domain,” the concept of a science became progressively more focused on its method than on its object. Or more exactly, the expression “object of science” acquired a new sense. The object of science is no longer only the specific domain of problems and obstacles to resolve, it is also the intention and target of the subject of science, it is the specific project that constitutes a theoretical conscience as such.
Georges Canguilhem, What is Psychology? (1956) [tr. David M. Peña-Guzmán]
Georges Canguilhem, What is Psychology? (1956) [tr. David M. Peña-Guzmán]
Got a reprint of this classic earlier this month. Good memories of learning exterior products for the first time from this. I wish/hope someone writes a biography of Spivak, always fascinates and inspires to know about people who dedicated their life to see the universe through the keyhole of a specific area. Spivak did that for all things related to geometry. A rare persona, and much rarer today.
I'll be reposting some posts from here and the other channel to my Mathstodon account, found some really good people and communities there. I'll eventually automate a bridge, but that has to wait until my self-hosting setup is ready.
Mathstodon
Divya Ranjan :hilbert: (@divyaranjan@mathstodon.xyz)
299 Posts, 349 Following, 186 Followers · Mathematics, Philosophy and Libre Software.
Lives inside GNU Emacs. GNU Guix package maintainer.
Lisps, Haskell, Rust, and occasionally C.
Formal verification, theorem proving, compilers, and anything that…
Lives inside GNU Emacs. GNU Guix package maintainer.
Lisps, Haskell, Rust, and occasionally C.
Formal verification, theorem proving, compilers, and anything that…
An (Very Short) Introduction to Differential Geometry and Curvature
https://functor.network/user/2326/entry/823
https://functor.network/user/2326/entry/823
Programming Deadlock
Recursive types for free! Philip Wadler https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt
INI Seminar Room 1 | Invidious
Prof. Philip Wadler | Interpreters for Free
Speaker(s) Philip Wadler University of Edinburgh
Date 8 July 2022 – 13:30 to 14:30
Venue INI Seminar Room 1
Session Title Interpreters for Free
Event [VS2W01] Vistas in Verified Software
Abstract
In a proof assistant based on intuitionistic logic, a standard…
Date 8 July 2022 – 13:30 to 14:30
Venue INI Seminar Room 1
Session Title Interpreters for Free
Event [VS2W01] Vistas in Verified Software
Abstract
In a proof assistant based on intuitionistic logic, a standard…
(φ (μ (λ)))
Contra Gödel: https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof
In a different sense, Tarski already had an axiomatic system for Euclidean geometry that was both decidable and complete. Godel's incompleteness theorem can't touch this axiomatization because it is not as expressive to include parts of first-order Peano arithmetic.
Moreover there is an algorithm to decide whether each theorem, lemma and sentence of the axiomatic system can be provable or not.
Moreover there is an algorithm to decide whether each theorem, lemma and sentence of the axiomatic system can be provable or not.
Wikipedia
Tarski's axioms
first-order axiomatization of a fragment of Euclidean geometry
WASM GC isn't Ready for Realtime Graphics
https://dthompson.us/posts/wasm-gc-isnt-ready-for-realtime-graphics.html
https://dthompson.us/posts/wasm-gc-isnt-ready-for-realtime-graphics.html
(φ (μ (λ)))
Transcript of Richard Stallman at the 4th international GPLv3 conference; 23rd August 2006
A reminder that Free Software is a socio-philosophical movement to promote and restore freedom in software computing. It's primary goal was and always will be to provide all the essential freedoms to the user of any computer program.
All other concerns are secondary, including those of compatibility and convenience. They are not pointless, they just cannot supersede the essential freedom. Too often we forget the philosophical importance, and we should not. A lot of what exists wouldn't be possible if we didn't stick to that philosophy, especially when our fight is against absolute monopolies operated by oligarchs.
We cannot cede the ground on any aspect, that which we cede, is an opportunity for the enemy. Moreover, a lot of us even have difficulty identifying our enemy since it's no longer the days of the feudal system, in modern-day neoliberalism our enemy pretends to be our closest friend. As recently we've seen from Daniel by keeping Pixelfed a fighting alternative against the malicious Instagram. Here indeed Zuckerberg and his companies are our enemy, no matter how many of our friends or relatives love it.
But as has been shown by luminary revolutionaries across history, whether it was Marx's thorough analysis of capitalism, or Stallman's analysis of the discontents of the copyright law; it shows that those in power do not care about our fundamental rights. And since they don't, we should!
And we need to be united here, united to fight for what's essential, fight for that which Marx long ago said is the commons. And today, digital commons is just as crucial, if not more, as commons in other media.
All other concerns are secondary, including those of compatibility and convenience. They are not pointless, they just cannot supersede the essential freedom. Too often we forget the philosophical importance, and we should not. A lot of what exists wouldn't be possible if we didn't stick to that philosophy, especially when our fight is against absolute monopolies operated by oligarchs.
We cannot cede the ground on any aspect, that which we cede, is an opportunity for the enemy. Moreover, a lot of us even have difficulty identifying our enemy since it's no longer the days of the feudal system, in modern-day neoliberalism our enemy pretends to be our closest friend. As recently we've seen from Daniel by keeping Pixelfed a fighting alternative against the malicious Instagram. Here indeed Zuckerberg and his companies are our enemy, no matter how many of our friends or relatives love it.
But as has been shown by luminary revolutionaries across history, whether it was Marx's thorough analysis of capitalism, or Stallman's analysis of the discontents of the copyright law; it shows that those in power do not care about our fundamental rights. And since they don't, we should!
And we need to be united here, united to fight for what's essential, fight for that which Marx long ago said is the commons. And today, digital commons is just as crucial, if not more, as commons in other media.
👍5
Software patents don't cover programs or code; they cover ideas (methods, techniques, features, algorithms, etc.). Developing a large program entails combining thousands of ideas, and even if a few of them are new, the rest must necessarily have come from other sources, such as programs the developer has seen. If each of these ideas could be patented by someone, every large program is likely to infringe hundreds of patents. Developing a large program means laying oneself open to hundreds of potential lawsuits. Software patents are a menace to software developers, and to the users. Since patent law covers execution of the program, the users can also be sued.
A few fortunate software developers avoid most of the danger. These are the megacorporations, which typically have thousands of patents each, and cross-license with each other. This gives them an advantage over smaller rivals not in a position to do likewise. That's why it is generally the megacorporations that lobby for software patents.
Richard Stallman, Bill Gates and Other Communists
A few fortunate software developers avoid most of the danger. These are the megacorporations, which typically have thousands of patents each, and cross-license with each other. This gives them an advantage over smaller rivals not in a position to do likewise. That's why it is generally the megacorporations that lobby for software patents.
Richard Stallman, Bill Gates and Other Communists
Guix is finally doing its Guix Consesus Document process, aka Request For Comment (RFC) process.
This would ensure a much more broader and democratic process to conduct the significant decision-making that goes into Guix development. This will ensure people from the community have a say on some core changes, both technical and otherwise.
The whole thing cane be tracked here.
P.S: If you're in a Guix team, you'd already get a CC of this mail.
This would ensure a much more broader and democratic process to conduct the significant decision-making that goes into Guix development. This will ensure people from the community have a say on some core changes, both technical and otherwise.
The whole thing cane be tracked here.
P.S: If you're in a Guix team, you'd already get a CC of this mail.
👍2