╭
𝟙𝟡·
I started my main project, ‘Sudoku by Proof’ before I discovered Lean Sudoku. I think it'll be fun to continue anyway. I've been slowly working through “Mathematical Logic through Python”
┊
while writing my own tools - even my own variants of programming languages! Still all a jumble, a little bit is starting to congeal and hopefully I'll make some consistent progress.
𝔽
┊
𝟚𝟞·
I'm easily distracted when programming by potential improvements to my ‘ecosystem’ (a friend put it nicely: “you're a tools guy”). I dogfed (dogfooded?) my Python and C preprocessor to itself
𝕖
┊
for the first time in a while and, well, it took the afternoon. ‘Zypp’ does really important things, like replacing some operators with more math-y versions available in Unicode: ‘&&’ in C
𝕓
┊
and ‘and’ in Python both get replaced with ‘∧’, which I use in my syntax for logical formulae I call ‘Sapphire’. I like minimalist punctuation and Python's visible block structure, so, among
┊
other less-critical things, Zypp inserts curly braces into my C code. Currently it's a total hack and gets changes and fixes constantly as I write new code - eventually I plan to create a
┊
parser and I'll more legitimately describe the code I write as ‘Midnight’ (the dynamic language formerly known as ‘hacked up Python’) and ‘Cobalt’ (the compiled language formerly known as
╰
‘really broken C’).
𝟯
/
𝟘𝟞·
When Peano's axioms are constrained to first order Logic, the Natural numbers cannot be defined precisely - they admit the interesting structure of non-standard arithmetic. But it's time to
┊
learn a bit about Reverse Mathematics, which works with second order Logic because, while the expressiveness has its burdens, feels non-negotiable.
╰
𝟙𝟝·
To encourage myself to get more done, I'm posting a bit or two from my Symbolic Logic project. A few simple propositional proofs as things currently stand.
𝟰
/
𝟘𝟠·
Hello World in the Spectrum languages Sapphire, Midnight and Cobalt. I added some fancy features to the empty Spectrum file I had posted, implementing solutions to that challenging problem
╰
Computer Science students usually don't see until 2nd or 3rd year!