flaviat

joined 2 years ago
sorted by: new top controversial old
Stubsack: weekly thread for sneers not worth an entire post, week ending 15th November 2026 in c/techtakes@awful.systems
[–] flaviat@awful.systems 3 points 1 day ago

Arguing over homeopathic doses of AI misses the point like with actual homeopathy. They used it.

Tesla Running FSD Slams Into Police Cruiser After Driver Falls Asleep Behind the Wheel, Hospitalizing Two Officers With Serious Injuries in c/techtakes@awful.systems
[–] flaviat@awful.systems 8 points 3 weeks ago* (last edited 3 weeks ago)

Complain about tesla drivers -> "how about holding the rich responsible instead of regular people"

Complain about tesla -> "the drivers were clearly not using them properly we should blame them"

Stubsack: weekly thread for sneers not worth an entire post, week ending 4th October 2026 in c/techtakes@awful.systems
[–] flaviat@awful.systems 10 points 1 month ago* (last edited 1 month ago) (1 children)

Projects that continue to prohibit AI-generated vulnerability reports are no longer suitable dependencies for GNOME

How. That ~~is~~ (E: was) the policy of curl and they are AI centrists.

As a programming newcomer AND a dyscalculic, which ones are the best programming languages to learn that aren't tainted by AI and the best resources to learn them? in c/freeasm@awful.systems
[–] flaviat@awful.systems 4 points 1 month ago (1 children)

I suggest Forth. It's a language where you manipulate stuff on a stack. You rearrange and duplicate things, operations happen to the elements on the top. You manage the variables in your head or on paper, where you can be as wordy or symbolic as you like.

Random Positivity Threads in c/morewrite@awful.systems
[–] flaviat@awful.systems 6 points 1 month ago

Our ISP decided suddenly to give us a public IP. I only need to fix an ethernet cable and I can capitalize on this. just a factorio server for now

Random Positivity Threads in c/morewrite@awful.systems
[–] flaviat@awful.systems 3 points 1 month ago

I couldn't finish it. This is too much for someone who definitely would have been thrown in there

Stubsack: weekly thread for sneers not worth an entire post, week ending 20th September 2026 in c/techtakes@awful.systems
Stubsack: weekly thread for sneers not worth an entire post, week ending 13th September 2026 in c/techtakes@awful.systems
6
Mikan proof assistant (codeberg.org)
 

Announcement of the Agda fork by amy@types.pl:

The Agda developers have recently proposed codifying their official stance on LLM-generated contributions: they are "concerned about the negative effects of large language models (LLMs) on many individuals, our society, and our planet", but refuse to take any concrete action to address their own contribution to these.

Other extensions to the type theory are kept despite known inconsistencies (sized types), or being impossible to adopt without complete vertical buy-in (cumulativity, erased cubical), or simply for backwards compatibility (--guarded/@lock). In the best cases, these features are championed by a single maintainer, and keeping them well-tested against the continuous adoption of new features is a struggle when very little code uses them. Our plan is to focus on exactly one variant of the language ("full --cubical"), and to drop support for all the language features which are explicitly deprecated, inconsistent, or simply ill-understood in conjunction with this fragment.

I tried it out using Amélia's library (https://1lab.dev/) to show that free modules are projective. This is known to be equivalent to the axiom of choice and that informed the definition of projective to have mere existence of the lifted homomorphism. It was pretty ergonomic, details regarding homotopy levels were handled by hlevel and universe levels weren't bad. Automatic proof search worked with a sufficiently fleshed out structure

Stubsack: weekly thread for sneers not worth an entire post, week ending 26th July 2026 in c/techtakes@awful.systems
[–] flaviat@awful.systems 5 points 3 months ago (9 children)

I just entered university for math and even though this is all very demotivating, it's just what I'm good at.

https://math.andrej.com/2013/08/19/how-to-review-formalized-mathematics/

The AI people's cry of "no don't look at the code! it's in lean so it's correct! does give me a bit of hope (hi bitofhope if you're here) that it's bullshit that will fall over

Stubsack: weekly thread for sneers not worth an entire post, week ending 5th July 2026 in c/techtakes@awful.systems
[–] flaviat@awful.systems 5 points 4 months ago

Smart Pipe Inc. is a Registered Sex Offender

Office workers are spending way too much on AI too in c/techtakes@awful.systems
[–] flaviat@awful.systems 5 points 4 months ago (3 children)

There cannot be such a thing since pdf does not structure its data. There is an extension to the standard that would let a program do it for you but nobody uses it (PDF/UA-1). (also pandoc is vibe coded now)

Antediluvian beast thought extinct spotted on Mars in c/buttcoin@awful.systems
[–] flaviat@awful.systems 5 points 5 months ago

+1 for Archipelago

view more: next ›