61 lines
3.2 KiB
Markdown
61 lines
3.2 KiB
Markdown
The quick brown fox jumps over the lazy dog. The dog stays blissfully asleep. :)
|
|
|
|
This time, I'm actually going to begin writing a journal. I feel like I have a
|
|
lot of thoughts that I let swim around, without doing much about them. To quote
|
|
*the Happiness Lab* episode that I listened to today:
|
|
|
|
"Good intentions mean nothing if they don't translate into actions."
|
|
|
|
So I'll take Dan's advice, and use writing to do thinking. I also think that
|
|
writing this journal can improve my writing skills.
|
|
|
|
So what's going on today?
|
|
|
|
Well as I'm writing this, I'm on the 61D on my way into school listening to
|
|
*Spanish Pipedream* by John Prine. But what I really want to tell you about is
|
|
the decision I'm trying to make about whether or not to finish my PhD here at
|
|
Pitt with Dan. Last Friday, I had a meeting with Dan about an idea I was
|
|
interested in pursuing that at the core involved working with a real, tangible
|
|
system. That idea was politely dismissed, and I was 'nudged' back towards formal
|
|
methods for critical infrastructure. My immediate impression is that formal
|
|
methods for our lab is a crock of shit.
|
|
|
|
Dan means well and is genuinely looking out for my best interest, but that
|
|
doesn't translate into belief into his mission. Formal methods are an intense
|
|
mathematical pursuit in order to prove 'correctness' of something to something
|
|
else. Formal methods experts may disagree with that characterization, but
|
|
ultimately that second 'something' can be a lot of things, such as a model of a
|
|
plant, a written specification, or anything that can be logically defined. Dan
|
|
wants to use formal methods to prove things about physical systems. His idea is
|
|
aligned with what Manyu just finished up: can we use formal methods to prove that
|
|
certain systems adhere to requirements using formal methods? This is connected
|
|
in part to the HARDENS report, which tried to use formal methods tools at several
|
|
layers of abstraction to prove that a written requirement can be translated into
|
|
a proof for a determined plant design. There is certainly work to be done there.
|
|
|
|
But is that work that I want to do? My brain says I could do it, but my gut
|
|
screams out a vehement no. This is the core issue--I know I could do it, but
|
|
once I would finish, where does that leave me? The answer: a formal methods
|
|
expert. Formal methods experts are highly sought after, but it is an intensely
|
|
theoretical oriented field. When I think about what I want to do in my career
|
|
and what my values are, they are not only working through a computer (despite
|
|
my aptitude for such). I want to build real things, works you can touch, and
|
|
that interact with the world. A formal methods proof about a reactor that *might*
|
|
get built is not in that alignment.
|
|
|
|
So what the hell do I do? As I write this, it seems pretty clear the relationship
|
|
between myself and the Cole Lab's work is fractured. Going forward, I see three
|
|
main options:
|
|
|
|
1) Find another PhD advisor at Pitt. Bajaj is an obvious choice.
|
|
2) Master out and go find a job.
|
|
3) Go find another PhD opportunity somewhere else. Yichen did this.
|
|
|
|
Pros and cons of each situation:
|
|
|
|
1) Find another PhD advisor at Pitt
|
|
+ I would be able to keep my NRC Fellowship
|
|
+ I know people here already
|
|
+ I've already passed the qualifying exam
|
|
|