danesabo/Obsidian
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

vault backup: 2025-03-07 16:18:52

Browse Source
This commit is contained in:
Dane Sabo 2025-03-07 16:18:52 -05:00
parent 1eeee2a621
commit fef25e65ee
1 changed files with 31 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
5 Thesis/2 Logs/0225Update.md
View File

@ -1,11 +1,37 @@
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.
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.
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 more 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.
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.
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.