Yes. I am rubber ducking on mastodon.

Princeton coder Bro's are... lol

Look at this madness.

Show thread

The new bane of my existence, uncommented Coq code.

Axiom ef_deterministic_fun:
forall ef,
ef_deterministic ef = true ->
forall ge args m t1 t2 vres1 vres2 m1 m2,
Events.external_call ef ge args m t1 vres1 m1 ->
Events.external_call ef ge args m t2 vres2 m2 ->
(vres1,t1,m1) = (vres2,t2,m2).

Gee thanks... Not only is one of the most conceptually complex languages mankind has come up with, it has that single letter fetishism that mathematicians tend to have.

The freeBSD logo :freebsd: looks a lot cooler than openBSD :openbsd:. So I have taken :freebsd: to mean BSD.

But Puffy has grown on me. Few people will understand why I have pufferfish everywhere. But whatever.

By lisp logic, code == data. So data engineers/scientists are software engineers/scientists.


This testing technique would probably be good to compare how *nix lego programs are working between operating systems.

IBM is pretty great. They invest so much money into open source and linux kernel development.

I kind of wish they didn't sell thinkpad rights to Lenovo though.

Logic programming:
- Coq, compilers, proof code, knowledge engineering

Math programming:
- tensorflow, ML and AI stuff, linear programming

Really miss GOFAI and lisp in AI. Guess it is time to open that topology book, before the engineers make planet killing AI from their lack of understanding of measure spaces.

*grumble grumble*

Show thread

So AT&T does not allow the Pinephone. Any phone companies that do?

They suspended my account as soon as they found out I was using the sim card with technology that didn't include spyware.

Kind of tired of new languages.

If I can do everything (including bounds checking, you rust babies) in one language, just let me. Having to google how to do basic things every 2 minutes is not a productivity gain.

AI is a buzzword.

It is literally just a programming style your professor thought was too complicated to teach you.

It is very much worth learning though. May future GPU's become cheaper.

Controlling for mental limitations seems to be a common theme in the formal sciences such as math and software engineering.

"In this paper, we have tended to stress simplicity above all else because that is the first filter for any proof."

Good mathematicians are suckless devs.

I don't understand my computer. But I "can" understand any part of my computer. I own it. It won't sell me out to suckerberg or the alphabet boys. *freedom flex*


Excuse the naiveté, but what is the deal with languages and operating systems that organize themselves around one feature? From an SE perspective, that seems like a lot of work to adapt your own compiler, or kernel and package system, over a single selling point.

For example:
Rust, memory safty
Haskell, lazy evaluation

Guix, hashed/functional package management
InstantOS, fast wm

Anybody here get into dwarf fortress?

Show more

A mastodon instance created by Derek Taylor, creator of the DistroTube channels on YouTube and LBRY. Derek is an advocate for free and open source software.