Magos Logis Logan @jmw150@qoto.org

Commutativity and associativity are some weird properties.

Like a few mathematicians I know like commutative algebra quite a bit more than the non-commutative stuff. Symmetry is nice because it is simple. But the basic element of vector spaces, and grammars, is that they are naturally non-commutative. It is like there is something about non-commutativity that does not scale I guess.

And associativity properties is basically the entire parallel programming research field in a nutshell. (at least the PL side, electronics is different)

Eh, I guess a lot of things are age old algebra with a different coat of paint.

The most successful area of AI is compiler theory.

I pretty anti-intelligence for someone that works in artificial intelligence.

Intelligence is not false. Just so much of the idea of it is an anthropomorphism.

It is weird how AI has a lot to do with programming language theory. Everything is always blending together in the formal sciences. The actual boundaries between topics are nuanced.

It is kind of like the feeling that math is all one subject, even though to an undergrad something like analysis and algebra might feel miles apart.

A lot of what I think makes a person seem smart, is their belief that they can overcome intellectual obstacles.

I guess I am publishing this semester after all. lel

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

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!

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.

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

Good general advice for academia

https://terrytao.wordpress.com/career-advice/

Interesting as always

https://waitbutwhy.com/2019/09/thinking-ladder.html