38 lines
2.3 KiB
Markdown
38 lines
2.3 KiB
Markdown
This is the first update I'm writing on my thesis progress. Of which there has been some,
|
|
but we're still in a murky place when it comes to what the thesis actually is.
|
|
This is also the first time I'm trying to formalize my thoughts on everything,
|
|
so this first update may be a little rough.
|
|
|
|
# What's been Done
|
|
|
|
This past month I've been learning a lot about several different programming languages.
|
|
These languages include Haskell, Rust, Lean, and TLA+ (though that last one is less of
|
|
a 'programming' language and more of a formal specification language).
|
|
The effort in learning all these different languages changes a little bit depending on the language,
|
|
but in general I'm justifying spending time learning all of these languages because
|
|
I think they'll be relevant to my future career. Let me explain.
|
|
|
|
First and foremost, I think Lean and TLA+ will be useful immediately in my PhD.
|
|
I'll discuss a little bit what my potential topic will be about later or in an idea note,
|
|
but first I can touch on why I think these are relevant. Lean and TLA+ are both
|
|
formal specification languages, although I've seen examples of Lean being used
|
|
for programming oriented things. TLA+ is a model checker, that takes in
|
|
logical specifications of programs as a temporal logic of actions, and then
|
|
uses the TLC model checker to check your specification against a model.
|
|
TLA+ is maybe something that could be very useful for regulations refinement, as being able
|
|
to specify comething in a Lean or TLA+ and connect them into the natural language can
|
|
provide a proof that a certain system meets specifications or
|
|
that a regulation is a closed, nonconflicting ordinance.
|
|
|
|
|
|
Rust is a little different. I think in the world of controls and instrumentation,
|
|
there is no way we're going to go away embedded programming--which is mostly done in C right now.
|
|
I won't prattle on about how C isn't memory safe, because that's basically lore at this point.
|
|
Rust sovles this issues. Also no prattling required. I just think it'll be useful
|
|
to know how to write Rust code when it comes to programing controllers.
|
|
I believe Rust also has support for functional programming...
|
|
|
|
Which brings me to my darling Haskell, of which I've only done 2 chapters
|
|
of the book so far. Haskell is a purely functional programming language,
|
|
which means that all variables are immutable and the programmer must control the magical monad.
|