Kind of curious about the emotional reasoning that people use when attempting to get at truth.

I don't think emotional reasoning is disingenuous.

My reasoning for how I valued math for example went in the opposite direction when it came into conflict with the design goals of logic. I made good arguments against value of math as an institution, but I only generated this to explain an existing value system. After I had time to compartmentalize, the value of the arguments lessened.

https://plato.stanford.edu/entries/value-theory/

Guessing at value is how I know some areas are worth spending years looking into. But if I were born with different inclinations, my search pattern would be different. So what are the right inclinations/instincts?

Types are Internal $\infty$-Groupoids. (arXiv:2105.00024v1 [cs.LO]) http://arxiv.org/abs/2105.00024

So.. a student complained about having a panic attack today. They had it over hearing honest accounts of how mathematical research is done, in a forum chat.

They wanted staff members suspended for a week to rectify this.

I feel for the person being that sensitive. But this is part of what pure subjects worry about. And I do not get that kind of cultural perspective of consumer and producer, instead of mentor and student.

The complicated ritual of getting into higher math cuts down on people that make everything political, like that at least. This is stuff that happens in 101 classes. So odd to see a senior turn on their near-colleages like that.

As of #OpenBSD 6.9 (or -current), you can now run the latest #Minecraft using #MultiMC 5 now available in the package repository. #runbsd #playonbsd #bsd

SPECTRE: Defending Against Backdoor Attacks Using Robust Statistics. (arXiv:2104.11315v1 [cs.LG]) http://arxiv.org/abs/2104.11315

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.

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.

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.

Good general advice for academia

Interesting as always

- OpenPGP
- DE88709FB5E39ED3021ED3A5DC9ABF0861F09E02

- Background
- Logic, Mathematics, Computer Science

- Hobbies
- Philosophy, Programming, Video Games

I am a logician.

At the end of the day, I think logic is a core discipline that helps us most when navigating the world and growing as individuals. There are other methods of understanding things. But logic is the most beautiful and powerful to me.

Career wise I am both a mathematics and computer science researcher (mildly tautological). My specific field is automated reasoning systems. This overlaps with the PL community (POPL/PLDI/OOPSLA), Formal Methods community (CAV/TACAS) and ML community (NeurIPS/ICML/ICLR).

But there is a lot to love in the modern sciences. I am slowly completing a masters level understanding of pure mathematics, physics, and philosophy. I like writing mathematical proofs in languages like Coq, programming language theory, AI systems, converging function spaces, higher structures, and foundational theories.

Pure math

https://hbpms.blogspot.com/2008/05/content-and-about.html

Physics

https://www.susanrigetti.com/physics

Philosophy (analytic stuff)

https://fuckyeahlogical.tumblr.com/post/128964910533/analytic-philosophy-reading-list-for-the-self

Joined Aug 2020