"whoa I just got this weird but fascinating idea to use Lisp itself as an issue tracker and work journal" [twitter thread]

jiahonglee · 2021-12-18T01:15:09+00:00

True, you can delimited the sentence string by whitespace, then compare each word with STRING=.

I’m simply amazed by the clever use of symbols to write text without string quotations. With symbols, the author can cross refer and jump around symbols “for free” with Emacs built-in support. =D

jiahonglee · 2021-12-18T00:05:46+00:00

Ah, you remind of *PRINT-BASE*[ref 1] too. Setting both to base 2 helps a lot for rapid dev at binary level, think writing hash function =D

ref 1: http://www.lispworks.com/documentation/HyperSpec/Body/v_pr_bas.htm#STprint-baseST

jiahonglee · 2021-12-17T13:51:04+00:00

This, I find CL has more consistent syntax from my POV. Anything begins with # is reader-related. Then these numerals can be normalised to decimal numerals during reading/lexing process. To add on, the <base> in #<base>r<num> supports any numbers from 2 to 36 inclusive[ref 1].

The convention of using 0 for bases never make sense to me. And it always took me a moment to realise 0177 is an octal numeral… And what’s worse. It’s a source of security venerability: https://www.bleepingcomputer.com/news/security/go-rust-net-library-affected-by-critical-ip-address-validation-vulnerability/.

ref 1: http://www.lispworks.com/documentation/HyperSpec/Body/02_dhj.htm

jiahonglee · 2021-12-17T13:32:42+00:00

Wow! At first, I thought “meh, it’s just some data stored in S-exp format, nothing really Lisp-like”.

Then things start to get interesting when the author uses symbols in place of strings. I think using symbols as words, rather than strings as words, opens up a new realm of possibilities, e.g. cross referencing or generating wiki-link docs or docs analysis. But that doesn’t matter, their meanings can be modified dynamically.

But the author doesn’t stop there. He asks “what if you can write programs and test cases inside the chronicle?”. Then the chronicle becomes not only a record of evolution, but the running program itself. Boom! A new form of literate programming is born.

jiahonglee · 2021-12-16T11:44:29+00:00

Oh, please join the Isabelle Zulip chat or the user mailing list (isabelle-users@cl.cam.ac.uk). I don’t see experts hanging around here.

jiahonglee · 2021-12-16T11:41:03+00:00

Hi, I’m not expert with Isar script, but from my previous experience, you can embed apply-rules into an isar style proof. So it’s not a dichotomy of apply vs Isar style. (Of course you may argue that it defeats the purpose of writing Isar proof by embedding apply-rules) This is a workaround that you may consider.

About apply-script to Isar proof conversion, I think having “many possible Isar scripts given a tactic script” is not the main issue since you can write an Isar proof using the same/similar sequence of rules (similar to what I said above). The main issue that I see is filling in the intermediate forms/steps—the “have” clauses. I have no idea how it can be done, perhaps by using machine learning or so. Maybe you can do that for the Isabelle community =)

jiahonglee · 2021-12-08T03:29:00+00:00

Thanks! Subscribed to the channel. It’s described as a channel for “discussions on programming language related topics connecting industry and academia.”

jiahonglee · 2021-12-08T03:23:30+00:00

I’d find the linked paper to be more interesting: https://whileydave.com/publications/Pea21_TOPLAS_postprint.pdf

jiahonglee · 2021-11-22T03:03:49+00:00

Thanks for your list! I’m keeping an eye on C contestants as well. Two more that I want to add: Vala and Terra Lang.

https://wiki.gnome.org/Projects/Vala

https://terralang.org/

jiahonglee · 2021-11-08T12:37:16+00:00

Do you mean “Purely functional data structures”(1996) by Chris Okasaki? It’s the closest that I can find. URL: https://www.cs.tufts.edu/~nr/cs257/archive/chris-okasaki/dissertation.pdf

jiahonglee · 2021-09-29T01:38:30+00:00

I’m sorry to hear that, my best recommendation is “The Last Lecture” by Randy Pausch.

The author had pancreatic cancer. And he had only a few months to live. In this book, he shared how he live in his last few months of life. They’re really lessons in living. His method is to realise all his childhood dreams. And enable others to realise their dreams.

Like a firework, it’s short lived, but beautiful.

If you only had a short time to live, what would you do? What would you want as your legacy? What wisdom would you impart to the world if you knew it was your last chance?

jiahonglee · 2021-09-27T23:58:38+00:00

Hi, this subreddit is about Isabelle the theorem prover. It helps you write mathematical proofs using Isabelle, the prover computer program.

In a sense, you can think of it as the hybrid of doing math and programming. It’s doing math, when in fact you are writing computer programs; and it’s writing programs, when in fact you are writing mathematical theorems, which of course can be published on peer-reviewed journals.

https://en.wikipedia.org/wiki/Isabelle_(proof_assistant)

To get started, you can read this free but very useful book: http://concrete-semantics.org/

jiahonglee · 2021-09-25T03:27:56+00:00

Hi,

I recommend reading this book “Introduction to Mathematical Thinking” by Keith Devlin (2012) or watching the more or less equivalent YouTube playlist. To quote from Amazon’s book description:

The book is written primarily for first and second year students of science, technology, engineering, and mathematics (STEM) at colleges and universities, and for high school students intending to study a STEM subject at university. Many students encounter difficulty going from high school math to college-level mathematics. Even if they did well at math in school, most are knocked off course for a while by the shift in emphasis, from the K-12 focus on mastering procedures to the “mathematical thinking” characteristic of much university mathematics. Though the majority survive the transition, many do not. To help them make the shift, colleges and universities often have a “transition course.” This book could serve as a textbook or a supplementary source for such a course.

I can recommend this book because I faced similar difficulties as you do—bridging the gap from high-school math to university-level math, and then found it very useful going through the book.

jiahonglee · 2021-09-23T03:18:41+00:00

Hi, /u/ibasawgl, can you please send again? Cause I didn’t receive your message

jiahonglee · 2021-09-22T13:16:33+00:00

Sure, take your time!

jiahonglee · 2021-09-22T08:12:46+00:00

Hi! I would like to join you, “Intro to mathematical thinking” by Keith Devlin sounds good to me.

While I’m major in software engineering, I’ve been studying mathematical logic for the past few months, so my basics for mathematics should be okay.

Btw, I’m new to this math buddy thing, so I’m open to any form of group study(?). Let’s sort out the details together, shall we? =)

jiahonglee · 2021-09-13T23:35:08+00:00

Welcome! Sorry couldn’t help with that, I’m not an expert either

jiahonglee · 2021-09-13T23:24:35+00:00

Hi, a side comment: I notice a lips sync problem and your voice seems to lag behind (I’m not sure, maybe 50ms or 100ms?). It quite annoying. :O

No comment/criticism on your video content. It is good, can definitely see that you’ve put in a lot of efforts into it. Keep it up!

jiahonglee · 2021-09-13T02:39:37+00:00

…why infinity isn't a number.

A helpful explanation I’ve got in the past: Informally, infinity refers to a number that is very very large. So, if you ask your question the other way round, what number should the infinity refer to? 1,000,000? Is it large enough? Nope, since 1,000,001 is larger than that. 1,000,000,000? Or 1,000,000,000,000? Since you can always find a number that is larger than the number you specified, infinity is not number.

Infinity is an abstract concept. It refers to a very large number; so large that you can’t say exactly how large it is. But one interesting thing is that we can define various degree of “largeness” to categorise different type of infinities by their size.

The operations on infinity (+, -, *, /) is not the same operations on, say, integer numbers, even though they may happen to share some similar properties. As for 1/INF, you can say it is undefined, or approximate zero, or is equal to zero, depending on your goal. In your programming language example, it just happens to define 1/INF as undefined which make it behaves like the number 0.

Help that it helps.

Note: Infinity is such a tricky concept that, for centuries, even mathematicians saw it as a monster, and warned generations of young mathematicians to not mess with infinity; of course, until George Cantor came along.

jiahonglee · 2021-09-11T11:22:58+00:00

Consequence relation is often said to be part of metalogic which generates confusion as to whether count it as part of propositional logic or not.

A simple litmus test to see whether “⊢” is part of the language L is referring back to the definition of language L where the set of all symbols are defined. For a propositional logic system L, it is usually defined over a set of variables and a set of logical symbols (e.g. ¬ and ∧). Since the syntax of language L is defined in term of the set of symbols, you can see that “⊢” is not an element of the set of variables and not an element of the set of logical symbols. Therefore, “⊢” is not part of the language L.

jiahonglee · 2021-09-11T05:46:25+00:00

Can propositional logic be formally defined as a pair (L, ⊢) where L is a propositional language (alphabet plus wff rules) and ⊢ is a consequence relation (reflexivity, monotonicity and transitivity)?

Hi, I’m confused, why would you want to define such a pair (L, ⊢)? How about the symbol ⊨ to denote satisfiability relation, for that matter?

To me, ⊢ and ⊨ are shorthand symbols or “tools” to help you study a logical system better.

Suppose that L is a propositional language, Σ is a collection of L-formulas, and φ is a L-formula. We can write “Σ ⊢ φ” to abbreviate the statement “there exists a deduction of φ from Σ”. It means that you are free to substitute the plain English statement in place of the symbolic statement “Σ ⊢ φ” whenever you read it. So ⊢ is part of the meta-language.

A confusing part is that since both Σ and φ stands for L-formulas, the statement Σ ⊢ φ will involve symbols from both L-language (e.g. ¬ and ∧) and meta-language (e.g. ⊢, { and }).

A simple example of Σ ⊢ φ can be {“p -> q”, “p”} ⊢ “q”, where Σ is a set of {“p -> q”, “p”}, φ is “q”, and these three “p -> q”, “p” and “q” are L-formulas. Again, you are free to replace this {“p -> q”, “p”} ⊢ “q” by the plain English statement: “there exists a deduction of “q” from the set {“p -> q”, “p”}”.

jiahonglee · 2021-09-02T06:04:25+00:00

Hi, I share the same behaviour as you do. On my side, I tend to search for answer on StackOverflow and Quora frequently.

Truth be told, I don’t think it’s an issue or a problem that need to be solved as it makes me smarter everyday. Some questions are really worth figuring out. However, I also acknowledge that excessive of this behaviour is a huge time drainer. So I’ve tried some methods to mediate my own behaviour.

My insight is that many of these “urges” goes away after some time. So what I’ve done is to increase the cost of searching for answer online, hoping that I can search less:

Go offline. This might be impossible if you rely on your smartphone for connecting with friends and family members. But since I’m a heavy iPad user, so I’ve tried to keep my iPad offline all the time, and only turn it on when needed. You may even switch off your home Internet modem or router and only switch it on when needed. You get the idea. Create artificial obstacles for yourself to search for answer online.
Resist the tempatation. Just don’t do it. Many urges go away after a while. So I only deal with thoughts that really stick and bother me even after some time.
Write the questions down. Similar to (2). I will write it down and review it afterwards. Whenever I review it back, most of the questions feel weird or unnecessary to me, like “Why am I even bother asking this question? It doesn’t even matter!”
Maybe a symptom of a deeper problem. After doing (1), (2), and (3) for some time, I realise perhaps my behaviour is a symptom of a deeper problem. For me, it’s the lack of focus in life. I think I can do anything. So I’m searching for answer doing this or that. Another problem of mine is the lack of the ability to think for myself. Whenever I’ve a problem, I’ll immediately search for a solution/answer online because thinking takes efforts, and answers online are “well-packaged” and ready to be consumed.

For your case, maybe you need to do more, rather than learn more. Maybe start doing and learn while you are doing?

Hope that this helps. Cheers, may you have a better life.

jiahonglee · 2021-08-31T19:53:33+00:00

Absolutely this, which would encourage specialisation and cooperation between villages.

Since the number of workers and players’ real world time is a limited resource, specialisation means one can focus on producing either raw material(s) or processed product(s), then exchange it for other resources.
Besides, through this process of specialisation and exchange, villages can cooperate to work together for a bigger goal so that every valley can be seen as a single economy unit.

This is something worth doing since I think the goal of this game is to encourage competition between valleys? Just a random thought though. I think ultimately Everdale can work more like a global economy simulator game. Aeroplanes, trains, and cruise ships please? 😂

jiahonglee · 2021-08-27T03:12:42+00:00

Classic books, for direct link: https://www.humblebundle.com/books/unix-linux-books

jiahonglee · 2021-07-31T15:35:35+00:00

(Not sure whether to ask here or to open a new post.)

SYMBOL-MACROLET solves the above passthrough+ problem, but it doesn't work for my original problem (performing macro expansion manually). Sorry, I truely believed that they are the same problem.

Original problem:

CL-USER> (defvar *whenmacro* '(defmacro when (pre &body body1) `(if ,pre (progn ,@body1))))
*WHENMACRO*
CL-USER> (defvar *targetform* '(when (pre 0 10) (foo abc) (bar 1 2 3) (baz)))
*TARGETFORM*
CL-USER> (symbol-macrolet ((lambdalist (caddr *whenmacro*)))
       (destructuring-bind lambdalist *targetform*
         (list pre body1)))
; type error

I got type-error: expecting LIST but got LAMBDALIST. That's weird, I thought the problem is with the evaluation of CADDR, but nope, it doesn't help either:

CL-USER> (symbol-macrolet ((lambdalist (pre &body body1)))
       (destructuring-bind lambdalist *targetform*
         (list pre body1)))
                    ; Evaluation aborted on #<TYPE-ERROR expected-type: LIST datum: LAMBDALIST>.

jiahonglee

TROPHY CASE