Share good ideas and conversation.   Login, Join Us, or Take a Tour!
ilex's profile

following: 5
followed tags: 14
followed domains: 0
badges given: 0 of 1
member for: 104 days
style: d20

comments 19

Hey, no need to be so hard on yourself. I see a younger me in the things you wrote, and certainly sometimes we all need to practice getting in front of disasters before they spiral out of control and make things even worse.

Things have been looking up over here lately. Hang in there. We're here for you.

Therapy tends to work if you've got a specific problem to solve / develop coping mechanisms for, but it sure isn't everything to everyone.


"Get your shit together lady and stop making it worse."

I have a partner I trust with most everything and close friends and chickens who love me unconditionally (as well as some handsome lab plants I am very proud of). I've got a degree in a technical field and another on the way. I have hobbies and projects and students to mentor. I have a lot of things to live for.

And yet.

There are days when the list of projects is more of a list of failures, the love and support from people close to me is an obligation for them, the work is an exercise in proving how incompetent and stupid I am. And I wake up with the knowledge that I should not be alive, that I am wasting all the effort and resources spent on me, that I'm a burden that can barely manage to feed herself. I go sit in my lab and try to focus but I can't really and nothing significant gets done, I go home and sit on the couch and stare into space and try to will myself to act a little bit like a human so the people around me don't worry and wait for the time to pass until I can sleep. I look at my week-long pill box and think about how much time is progressing and I am not.

I feel like shit for not accomplishing anything and I feel like shit for feeling like shit instead of accomplishing something anyway and I feel like shit get the idea. For me, this article is about stopping that spiral before it gets really deep. About just existing in that state, rather than agonizing over it too.

Every night I say goodnight to my chickens and shut them up in the coop. On my way back in, I stop by where we bury the ones who didn't make it and say goodnight to them too.

ilex  ·  link  ·  parent  ·  post: Pubski: August 21, 2019

Hello! I hope you all are doing well! I've been busy:


Finished up a paper that will hopefully be in print very soon. That project is switching directions a little bit, which means that we're working with another research group that has a 70kV EMI radiation setup. Looking forward to running some tests with it if we can keep it from destroying the computers we're testing on...


Installed a new water pump which required quite a bit of hand-fitting. Whoever machined the casting on it was not having a good day.

You'd be amazed how much quieter my truck is now that the water pump doesn't have a quarter inch of play in the shaft!

It feels like most Coq documentation and tutorials are written for people getting Ivy-league graduate degrees where they can just pop over to any number of professors or fellow students to ask a quick question or get a decent idea of what the "right" way to do something is.

Not having any of that, it's a bit tricky. I started very simple, proving basic logic statements and getting the hang of those tactics, then branched out a bit into proving things about numbers and lists. A fair bit of that came from Coq in a Hurry.

From there, Coq'Art is a dated but good resource for the questions Coq in a Hurry doesn't answer. Most of the proofs mostly work, but some of the tactics are different now?

However, even with those resources, I still find myself spending a lot of time looking around on the internet, finding bits and pieces in various disorganized places. Coq's standard library documentation is also horrendous and the various search commands in the language sometimes miss things for no apparent reason. And the error messages are only marginally useful.

That said, once you get a feel for its eccentricities it is pretty fun, and learning it has helped me get better at writing proofs even in informal settings!

Anyway, all this is to say maybe I should have learned Agda but I have to learn emacs first before I can make a fair call there :D

I also find this way cool. You will probably enjoy Wadler's Propositions as Types if you want to understand the proof/program thing in more detail.

I am generally interested in program analysis and theorem proving and that sort of thing. I picked it up to maybe use it with my research, since being able to generate proofs and extract executable code is pretty handy, but we'll see if I can become competent in it fast enough to be able to actually apply it.

Also I like roosters

I did write another thing about using Coq that shows some of the proof state as you go. The interactive part really makes writing proofs possible; I don't know if I could just look at something and write all the ltac for it without any help. This is a bit more along the lines of what I'm doing for research, but still a long ways from what counts as cutting-edge nowadays :)

I don't think coq is intuitive to anyone :) It might have the steepest learning curve of any language I've learned, possibly tied with Idris, which just so happens to be another dependently typed language.

The bits between Lemma and QED are kinda neat -- they're "proof tactics" written in the tactic language LTAC. It's kind of a metalanguage that directs Coq through synthesizing an actual program.

Like, for example, here's a simple proposition written in LTAC:

  Lemma fst : forall a b, a /\ b -> a.

intros a b [Ha Hb].

exact Ha.


and here's what Coq synthesizes for that:

  fst = 

fun (a b : Prop) (H : a /\ b) => match H with

| conj Ha _ => Ha


: forall a b : Prop, a /\ b -> a

(fun is the keyword for lambdas, kinda like \ in Haskell.)

In other words, that stuff is both program and proof!

ilex  ·  link  ·  parent  ·  post: Who Is Left on Hubski? (Part II)

It seems like I see a lot of Big Topics posted here (politcs, econ, etc.) and most days it can be pretty hard to have something insightful to say about them. There are plenty of topics that aren't quite so daunting -- and might lead to more conversation and balance out some of the more heated stuff?

ilex  ·  link  ·  parent  ·  post: Who Is Left on Hubski? (Part II)

Hey I really appreciate your supreme court roundup posts. It's nice to know what's going on there!

ilex  ·  link  ·  parent  ·  post: Who Is Left on Hubski? (Part II)




Middle of the woods in the rural midwest


Bit shy of 30

Current Preoccupations

Finishing grad school, finishing writing a book, finishing reading many books, finishing fixing one of my MR2s, etc.

Permanent Preoccupations

Learning to love my wife, my metamour, and myself better. Transition.

Previous Preoccupations

Surviving grad school, transition again (but faster)

    What change would you like to see from the users of Hubski?

More OC! And more not-serious conversation?

ilex  ·  link  ·  parent  ·  post: Labor Econ Versus the World

This sums up pretty exactly what growing up in a fundamentalist conservative christian household is like. There are things you just don't question and if you even try, the resulting discussion is so bad-faith and full of rabbit holes that you might as well not even bother. Unless you can find someone your parents already think speaks the gospel truth, you'll never convince them of anything, and even if you do the odds are that they'll denounce that person too.

I'm trying to learn how to speak more confidently and y'all (and especially KB) have definitely helped me see how that can look. (Although I don't think the bombast-and-cursing style will ever quite work for me!)

posts and shares 3/9