37 lines
2.1 KiB
Markdown
37 lines
2.1 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?
|