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

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.


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?

I guess I am publishing this semester after all. lel :blobwizard:

Types are Internal $\infty$-Groupoids. (arXiv:2105.00024v1 [cs.LO]) 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.

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

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

Ever think "ah, screw it" and want to just toss an abstract syntax tree as an argument for your program problem? Constraint based programming might be for you!



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


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

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

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.

:blobfoxcofe_w_: 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. :blobcatmegumin:

I agree with everything on this chart.. People tend to have the risks of an "AI war" in the future all backwards...

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


From here

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

- 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
vres is result value
m1 for memory state after call

Show thread

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.

Show more
Qoto Mastodon

QOTO: Question Others to Teach Ourselves. A STEM-oriented instance.

An inclusive free speech instance.
All cultures and opinions welcome.
Explicit hate speech and harassment strictly forbidden.
We federate with all servers: we don't block any servers.