Magos Logis Logan @jmw150@qoto.org

@freemo looks still to me.

It is odd how some of these don't work on kids. I think we eventually learn some shortcuts for our vision.

The ergonomics of modern proof writing just get better and better.

This is just a proof about a C program. Nothing in the program is important from a philosophical standpoint. But the logic and implementation is swell.

The logic is called higher-order impredicative concurrent separation logic. The separation part allows me to only have to think about small parts of the C program at a time. Multiple people can work on the same proof without stepping on each other.

The implementation allows for a lot of automation in proof writing. Most of the heavy lifting and boring stuff, like interfacing integers to registers of 64 bits are done. There is plenty of room to create more automation for common proof strategies.

@Snowermers tests are very important. You could spend a day learning about doing different types of test coverage.

*mathematical sophistication intesifies*

https://dl.acm.org/doi/10.1145/3297858.3304037

A more secure hardware design with risc-v

@gnull I am guessing you need Zoom for work. But I would not recommend it. Zoom has terrible security and a bunch of Spyware on it.

@zpartacoos I think it is an okay language. But it is over-marketed, and the language is not what it advertises itself as.

That makes it irritating for me because I get a bunch of new, or not very smart, programmers recommending it.

So I make it a point to nip rust hype in the bud. Languages like Ada are safer and standardized, if you are aiming for reliability. Plenty of other things in Rust already exist in other languages or tools as well.

@MindOfJoe @fribbledom

Yeah. It is really fancy now. The language is huge.

Also C has evolved away from it. So it is no longer a C superset.

@fribbledom

But that said, I like language design. C++ is kind of cool, if you can get devs to behave and only use 1 portion of it at time.

And hardware diverse systems tend to have nearly C compliant compilers instead of standard ones. C++ is something you would find on a fancier system.

So the statistics are not really true. We use C-ish language to avoid straight binary or assembler language. And this is due to C compilers being easy to write. But LLVM and the like may change this.

@fribbledom Which is pretty much just C.

You should see the development times with C projects vs C++ projects. C programming takes less time to get things done than C++ programming does on average.

It is not intuitive, but engineers only need 1 or 2 simple ways to make a piece of hardware do things in the first place.

In embedded systems, about 70% of the programming share is still C as of 2018.

https://barrgroup.com/sites/default/files/downloads/barr_group_2018_embedded_systems_safety_security_survey.pdf

@johnabs Hmm. I meant to say large groups of people think in a very different way in aggregate than individuals.

People also distrust large groups with complex goals, like governments, and other non-business organizations as they get bigger.

Fun language. Makes some proof programming easier.

https://rise4fun.com/Dafny/tutorial/Guide

If it does not have an objective function, it's not really intelligence.

But most things have this. So most things are intelligent. Much like most things are computers via the finite state machine model.

I think the reason some political groups distrust corporations is because such corporations count as a different kind of intelligence.

Some of these reasons are also similar to the distrust of AI.

@weinshec good to meet you. Rust is a stupid language though.

@anarchismnews@newsbots.eu minecraft? Was this generated by a bot?

@swiley You haven't read Karl Marx. Stop being such a brainlet.

@lucifargundam I had the same issue. Kind of over having cell tower dependency anyway.

@Diptchip Yeah probably. The black plague ended feudalism. But now we have robots. Supply and demand curves for labor is fucked.

@swiley I am giving a prediction based on current research papers that I am reading. I do not have to defend it to a bullet proof degree, and would not really have a method to do so. So we may never agree.

Maybe things will be fine. Maybe everybody can enjoy a star trek money free existence and do nothing of importance all of their lives, just breed and consume resources forever.

Or maybe people are dicks, and everyone is eventually fucked if they do not own stock in companies.

AI can fake anything from art to help desk work. I do not care enough to pay for the real thing. Do you?

@swiley Get bosses coffee for the sake of resume boosting. Some people have real adult jobs. Those are what are in jeopardy.

Here is some data on what I am saying

https://www.bls.gov/ooh/computer-and-information-technology/computer-programmers.htm