Shamar @Shamar@qoto.org
Joined May 2019
For the first time in her whole life, my eldest daughter is studying a discipline I don't know.
I find this rather disturbing.
Holding my breath... first try to compile GCC 9.2.0 for #Jehanne...
Shamar
boosted
working on a port of #NixOS 's NAR format for #Plan9 for a future purely functional package manager in the spirit of #Guix .
did you know that the #9front compilers have warnings for binary shifts that exceed the integer type's width? /bin/5c is surprisingly user friendly sometimes. (but the syntax errors could still use some work)
Shamar
boosted
How can you not label a country as ”authoritarian (racist) regime” when you see this militarized police equipped like that when they come to look for immigrants…
(yes, this is ICE in the USA...)
Source : https://twitter.com/RidgewdTenantsU/status/1192262495974678529
Shamar
boosted
@Drezil I think there's a bit of miscommunication going on here. What I'm thinking about is if there is a proper, formal way of stating and proving the Curry-Howard correspondence (which I interpret as in the attached picture).
What you're giving me are specific examples/corrolaries, which while very exciting and often insightful, are not really what I'm looking for.
2019-11-07-120831_833x333_scrot…
What you're giving me are specific examples/corrolaries, which while very exciting and often insightful, are not really what I'm looking for.
2019-11-07-120831_833x333_scrot…
Shamar
boosted
@Drezil I do know what the Curry-Howard correspondence is, I'm just wondering if there actually exists a properly stated theorem (that actually corresponds to our intuition of CH) with a proper proof. Of course it's (relatively) easy to state and prove for any specific combination of logic and type system, but I'm wondering if there is a way to state the correspondence generalized over logics and type systems.
Shamar
boosted
Interesting question: What kind of thing is the Curry-Howard correspondence? It's not a theorem, because you usually don't state it formally, right?
As a weirdly weird person, I respect everybody, weird and non-weird, from all over the world.
BUT as far as I can see, #US non-weird people are (being manipulated so that they are) actively working to further marginalize weirdos.
The fact is that living and working with weird people is going to be weird by definition.
People can accept this and adapt to such weirdness or refuse this and expel us.
For a few decades #FreeSoftware has been a sort of "safe place" for weird people. Even because of people like #RMS (which I consider moderately weird, actually 😉).
For sure, some exploited such safety to misbehave, but these were not #hackers, but #crackers posing as such (for proper definitions of these terms look at http://www.tesio.it/documents/vademecum.txt )
And now that Free Software is fundamental to #business and has a huge economical value, giving access to actual #Power, the #OpenSource lip service isn't enough anymore and some urge to redefine free software as something that is... less weird (in US #corporate perspective, obviously, as many US people can't think about different perspectives).
I don't think this is going to improve the life for non-weird people (as most of them are basically oppressed people that internalized the oppressors' values themselves and thus heartily and unconsciously support the oppression system).
But it will increase #conformism, further marginalizing us.
Venture Capitalist vs Hacker (fictional, but I guess it would be pretty realistic)
VC: Think big!
H: So, I have this protocol and this distributed operating system designed to replace primitive systems (#Windows, #Linux, #MacOS, #iOS, #Android...) and the #Web. But it's just the first step: the actual goal is to allow all people to program and debug their own software as they can read and write...
VC: Fine, fine, but what's the #BusinessModel?
H: 🤦♂️
I get it.
It's fine if you are going to contribute the JSON writer to Chibi, but you should talk about this with the author.
There are several trade offs, if you think about it.
For example reading JSON is much more frequent than writing it, so performances matter more.
Also there are several ways to design the API of a JSON writer, while there is only one way to read it.
Yeah!
Even #Assembly is very strongly typed! 🤣
(seriously! 😉)
Anyway, I meant it lacks user defined data types and static type checking.
While I get how this would probably break homoiconicity, I feel coding without type checking... dangerous.
BUT, I have to say that when I was a young #Emacs user I didn't feel such issue.
re: gnu drama
Mind to define "positive change"?
For example I would consider very positive if #GNU becomes less and less welcoming to #US corporate #hypocrisy.
Actually we should look for the #weirdest people to join, as #RMS is not #weird enough to me.
____
BTW, are you going to block/mute me too?
Beware: I'm not from the #US?
I dare to be #Italian!
____
Sorry for the #sarcasm, but I've found this https://guix.gnu.org/blog/2019/joint-statement-on-the-gnu-project/ as a political abuse against my people.
You are marginalizing #hackers because they are weird.
You joint a mob lynching #RMS for what he said, forgetting that #software is a form of human expression, so #FreeSoftware IS #FreeSpeech.
Well, while I don't want to discourage ANY sort of experimentation, remember the task at hand is to reduce the #Jehanne build complexity by getting rid of #GoLang.
Why?
My hope is to lessen the cost of going self hosted with Jehanne, as #Chibi is way simpler to port than GoLang.
If you write in standard (aka POSIX) C, we will have to port it to Jehanne separately (and to build the Chibi to link it even on Linux)
Maybe a #Scheme JSON writer would run unmodified on all systems.
____
Having said that... HAVE FUN! 😉
👴 <-- me, nodding...
NOTE: "scaring" does NOT mean "bad". 😉
Joined May 2019
