Magos Logis Logan @jmw150@qoto.org

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

So I usually speak against just letting companies have your data. This is one of the reasons why. Data might seem harmless, but it is often rich with inference-able structures. Not to mention this kind of data does not deprecate.

Original research
https://arxiv.org/abs/1611.04135

Article overview with less math-speak
https://www.technologyreview.com/2016/11/22/107128/neural-network-learns-to-identify-criminals-by-their-faces/

So..

- Your face alone could give away that you are an independent thinker, had an atypical childhood, or anything that puts a criminal record on you in China.

- Law abiding citizens in tend to all look like each other.

The 21st century is weird. It seems like every time I think of a cool research direction, I look for some literature and find a whole team of people doing just that.

Yeah, there are totally 7+ billion of us. So, for example, over 140 million people could get into Mensa. Not that Mensa is a criteria for intelligence itself. But it kind of demonstrates the point that there are potentially a lot of smart people out there.

Science is being done at a rapid pace. So much stuff is being done that people in the same field cannot keep up on the literature and end up accidentally repeating research results.

I think there is plenty of value to not trying to be original in the mess of it. A researcher probably could take the time to be thorough, or to organize and digest.

Interesting series. Security and verification go really well together.

https://www.youtube.com/playlist?list=PLA6Ht2dJt3SITo6PYTyzr9832epkyFD48

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.

*mathematical sophistication intesifies*

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

A more secure hardware design with risc-v