Magos Logis Logan @jmw150@qoto.org

@skells We told him that proof by contradiction is still allowed because it was in the past, before the 1800s, when logic started to mix with mathematics. And that they are in fact separate but related subjects.

Him and one other person had an autistic fit over that I guess.

FML

@claudiom@mastodon.sdf.org yas!!

@djoerd that is much more accurate. Scihub forever!

I leave the house for 5 minutes and I hurt my back. Guess what I am doing for the rest of the day.

@MutoShack@functional.cafe "Fresh out. Can I offer you more proprietary over-specialized hardware?"

@whirli what a weird country

@kakure

"ad tech industry" has plenty of reasons to grow outside of direct online ads (that any decent adblocker would block anyway).

The data can be used to understand the psychology of people and generate software tools. Tech companies can read this data and know what people want before attempting to create a product. Data is deep. This is called the information age now because statistics informs almost all practical choices.

Well I tasked myself with 6 days to implement this for a C program verifier.

https://arxiv.org/abs/1910.09521

Probably only going to manage one teeny component. But monadic second order logic, man.

This summer's projects are going to involve algebraic topology somehow. I do what I want!

@feld some IBM manager is in trouble for overstepping.

I know people that work for IBM. That is not a policy they have with software engineers in general.

Maybe it is just me, but I noticed that the few skills I carry around after years of study are things that I physically did and pretty much only that.

I did a lot of programming. I did a ton of thinking about and working with mathematics.

But I could not tell you about much about anatomy, even though I spent hours reading medical books as a child.

Well, less than a month to go in this semester already.

I thought I was going to publish this month, but nooo... Ah well. What a beautiful metaphysical reality to exist in. We members of the formal sciences are basically modern wizards.

@stux

@fribbledom I think system76 was selling a computer with 1TB of ram.

I was tempted to buy. Lol

Got to love that the Coq language documentation includes the syntax trees. I know I am dealing with adults. lol

@jmw150

From here
https://github.com/PrincetonUniversity/VST

What I can guess is that:

ef_deterministic_fun is a rule for external functions that are deterministic to tell if they are equivalent. This is for software that is used to formally prove that C programs are doing what we think they are.

Not sure why 'fun' is added at the end. It is common shorthand for function. But anyway, next bit:

This is the function ef, if this boolean function comes back true, these other conditions are true.

Definition ef_deterministic (ef: external_function) : bool :=
match ef with
| EF_external name sg => false
| EF_builtin name sg => true
| EF_runtime name sg => false
| EF_vload chunk => false
| EF_vstore chunk => false
| EF_malloc => true
| EF_free => true
| EF_memcpy sz al => true
| EF_annot kind text targs => true
| EF_annot_val kind Text rg => true
| EF_inline_asm text sg clob => false
| EF_debug kind text targs => true
end.

- What is 'ge'? Global environment?
- args are probably arguments
- m, m1, m2 are a mystery, I am guessing either a stack or a heap
- t1, t2 maybe stack or heap
- vres maybe a command of some sort

Thankfully Inria people are better at things. Probably because they are selling the C compiler, and can have professionals instead of students.

ef external function
ge global environment?
args to the function
m for memory state before call
t1?
vres is result value
m1 for memory state after call

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.

#VST #Coq #hire_a_software_engineer