on master help sign in
posts/precepts, main.scss: edited some quote formatting, added new styling for blockquotes
157e796édouard
content/blog/precepts-discussion.md+39−40
@@ -1,10 +1,10 @@
1+++
1+++
2title = "Precepts: Discussion"
2title = "Precepts: Discussion"
3−date = 2020-03-14
3+date = 2020-03-18
4−description = "Urbit is a principled approach to system design and programming, but it's often not obvious what those technical principles are. This is a list of the technical maxims that define Urbit's approach to engineering."
4+description = "The precepts aren’t arguments. We discuss and justify them here."
5[extra]
5[extra]
6author = "Philip Monk"
6author = "Philip Monk"
7−ship = "~wicdev-wisret"
7+ship = "~wicdev-wisryt"
8image ="https://media.urbit.org/site/posts/essays/discuss-01.jpg"
8image ="https://media.urbit.org/site/posts/essays/discuss-01.jpg"
9+++
9+++
10
10
@@ -210,22 +210,22 @@ case correctly than to "snap" to the nearest elegant formulation.
210
210
211> A11: Be simple and uncompromising in defining what's correct; go crazy
211> A11: Be simple and uncompromising in defining what's correct; go crazy
212> with optimizations.
212> with optimizations.
213−>
213+
214−> Nock is a great example of this. It contains the character of the
214+Nock is a great example of this. It contains the character of the
215−> virtual machine, but its asymptotics are bad. Add jets to fix the
215+virtual machine, but its asymptotics are bad. Add jets to fix the
216−> asymptotics.
216+asymptotics.
217−>
217+
218−> Another example is the ACID nature of Arvo. Arvo is a pure
218+Another example is the ACID nature of Arvo. Arvo is a pure
219−> function f(logs) of its event log, so formally Arvo is just a
219+function f(logs) of its event log, so formally Arvo is just a
220−> function run against an event log. A naive implementation has
220+function run against an event log. A naive implementation has
221−> very bad asymptotics; processing each new event is O(n) in the
221+very bad asymptotics; processing each new event is O(n) in the
222−> number of historical events. Choose the function g(state,log)
222+number of historical events. Choose the function g(state,log)
223−> such that f(logs ++ log) = g(f(logs),log). Then, as long as you
223+such that f(logs ++ log) = g(f(logs),log). Then, as long as you
224−> keep the state in memory, processing each new event is constant in
224+keep the state in memory, processing each new event is constant in
225−> the number of previous events. This still requires O(n) restart
225+the number of previous events. This still requires O(n) restart
226−> from disk, but you can also periodically (and non-blockingly)
226+from disk, but you can also periodically (and non-blockingly)
227−> write a checkpoint of the state to disk, so that restart from disk
227+write a checkpoint of the state to disk, so that restart from disk
228−> is only linear in the number of events since the last checkpoint.
228+is only linear in the number of events since the last checkpoint.
229
229
230This pretty much says it all. Define what's correct in as simple of
230This pretty much says it all. Define what's correct in as simple of
231terms as possible — this will make it easier to implement and reason
231terms as possible — this will make it easier to implement and reason
@@ -394,8 +394,7 @@ A perfect static type system can guarantee `T` is a subset of `S` — if it type
394
394
395Dually, a perfect testing suite can guarantee that `S` is a subset of `T` — no correct program fails the tests. This is vacuously true if you have no tests, for then `T = U`. So you want `T` to be as small as possible while still being a superset of `S` — you don't want to reject valid programs if you can help it. But you can't make `T == S` — there will always be some programs that are invalid but pass your typechecks (at least, if your program requires a Turing machine).
395Dually, a perfect testing suite can guarantee that `S` is a subset of `T` — no correct program fails the tests. This is vacuously true if you have no tests, for then `T = U`. So you want `T` to be as small as possible while still being a superset of `S` — you don't want to reject valid programs if you can help it. But you can't make `T == S` — there will always be some programs that are invalid but pass your typechecks (at least, if your program requires a Turing machine).
396
396
397−(It is possible to create a static type system that has `S` subset `T` property described above for a testing suite — see Erlang's Dialyzerand (related
397+(It is possible to create a static type system that has `S` subset `T` property described above for a testing suite — see Erlang's Dialyzerand [related work](http://user.it.uu.se/~tobiasl/publications/contracts.pdf).)
398−work)[http://user.it.uu.se/~tobiasl/publications/contracts.pdf].)
399
398
400A dynamic type system tells you neither of these ahead of time. Instead, you end up with type errors at runtime. Errors at runtime must be handled at runtime, when the programmer is not present. Errors at compile time are handled at compile time, when the programmer is present.
399A dynamic type system tells you neither of these ahead of time. Instead, you end up with type errors at runtime. Errors at runtime must be handled at runtime, when the programmer is not present. Errors at compile time are handled at compile time, when the programmer is present.
401
400
@@ -424,17 +423,17 @@ Better to define rules in a more powerful language. This allows you to follow A6
424Good code is the result of people approaching the act of engineering with the right attitude.
423Good code is the result of people approaching the act of engineering with the right attitude.
425
424
426> C1: Code courageously.
425> C1: Code courageously.
427−>
426+
428−> If you avoid changing a section of code for fear of awakening the
427+ If you avoid changing a section of code for fear of awakening the
429−> demons therein, you are living in fear. If you stay in the
428+ demons therein, you are living in fear. If you stay in the
430−> comfortable confines of the small section of the code you wrote or
429+ comfortable confines of the small section of the code you wrote or
431−> know well, you will never write legendary code. All code was
430+ know well, you will never write legendary code. All code was
432−> written by humans and can be mastered by humans.
431+ written by humans and can be mastered by humans.
433−>
432+
434−> It's natural to feel fear of code; however, you must act as though
433+ It's natural to feel fear of code; however, you must act as though
435−> you are able to master and change any part of it. To code
434+ you are able to master and change any part of it. To code
436−> courageously is to walk into any abyss, bring light, and make it
435+ courageously is to walk into any abyss, bring light, and make it
437−> right.
436+ right.
438
437
439The unix/internet stack is a giant ball of mud. It's so big that when you're standing on it, it looks like a bog, and it's not clear that there is a bottom to it. You know there must be, but it doesn't matter because you learned long ago that the best solution is to not dig too deep. Build a strong structure by spreading out your weight and using strong construction materials. If there's something useful deep in the mud, it's probably not worth diving in to pull it out. That's dangerous and prone to failure, and you know many people who have gotten stuck down there.
438The unix/internet stack is a giant ball of mud. It's so big that when you're standing on it, it looks like a bog, and it's not clear that there is a bottom to it. You know there must be, but it doesn't matter because you learned long ago that the best solution is to not dig too deep. Build a strong structure by spreading out your weight and using strong construction materials. If there's something useful deep in the mud, it's probably not worth diving in to pull it out. That's dangerous and prone to failure, and you know many people who have gotten stuck down there.
440
439
@@ -445,14 +444,14 @@ Urbit is small enough that, while there's definitely some construction-related d
445This property is worth fighting for. It's the whole reason Urbit was written. New Urbit programmers are instinctively distrustful of anything below them and code defensively and fearfully. They must learn that it's all drastically simpler and more legible than they're used to. It's still hard, but you can actually make progress. To do so, you have to stand up straight, so you can get a firm footing on the ground. Keep your chin up and your shoulders back, and adopt the posture of a conqueror. When something doesn't work right, don't retreat into your shell of safety and control — fix it. The forces of chaos are always lurking, but their victory isn't inevitable. It's all on the line, so code with abandon.
444This property is worth fighting for. It's the whole reason Urbit was written. New Urbit programmers are instinctively distrustful of anything below them and code defensively and fearfully. They must learn that it's all drastically simpler and more legible than they're used to. It's still hard, but you can actually make progress. To do so, you have to stand up straight, so you can get a firm footing on the ground. Keep your chin up and your shoulders back, and adopt the posture of a conqueror. When something doesn't work right, don't retreat into your shell of safety and control — fix it. The forces of chaos are always lurking, but their victory isn't inevitable. It's all on the line, so code with abandon.
446
445
447> C2: No time for lazy people.
446> C2: No time for lazy people.
448−>
447+
449−> If there's clearly a right way to do something and a wrong way, do
448+If there's clearly a right way to do something and a wrong way, do
450−> it the right way. Coding requires incredible discipline. Always
449+it the right way. Coding requires incredible discipline. Always
451−> follow conventions, and fire anyone who won't. Anything that can
450+follow conventions, and fire anyone who won't. Anything that can
452−> be solved by discipline is not a real problem.
451+be solved by discipline is not a real problem.
453−>
452+
454−> "To him who knows to do good and does not do it, to him it is
453+> "To him who knows to do good and does not do it, to him it is
455−> sin."
454+sin."
456
455
457Preserving the property of solid ground requires perpetual discipline. Once lost, it's often impossible to reacquire. Don't compromise your standards.
456Preserving the property of solid ground requires perpetual discipline. Once lost, it's often impossible to reacquire. Don't compromise your standards.
458
457
content/blog/precepts.md+4−4
@@ -1,10 +1,10 @@
1+++
1+++
2title = "Precepts"
2title = "Precepts"
3−date = 2020-03-14
3+date = 2020-03-18
4−description = "Urbit is a principled approach to system design and programming, but it's often not obvious what those technical principles are. This is a list of the technical maxims that define Urbit's approach to engineering."
4+description = "Technical maxims that define Urbit's approach to engineering."
5[extra]
5[extra]
6author = "Philip Monk"
6author = "Philip Monk"
7−ship = "~wicdev-wisret"
7+ship = "~wicdev-wisryt"
8image ="https://media.urbit.org/site/posts/essays/pre-01.jpg"
8image ="https://media.urbit.org/site/posts/essays/pre-01.jpg"
9+++
9+++
10
10
@@ -196,7 +196,7 @@ We’ll start with a brief description of many principles, then we’ll go into
196 follow conventions, and fire anyone who won't. Anything that can
196 follow conventions, and fire anyone who won't. Anything that can
197 be solved by discipline is not a real problem.
197 be solved by discipline is not a real problem.
198
198
199− "To him who knows to do good and does not do it, to him it is
199+ > "To him who knows to do good and does not do it, to him it is
200 sin."
200 sin."
201
201
2023) When a smart person makes an obviously stupid suggestion, before
2023) When a smart person makes an obviously stupid suggestion, before
sass/_main.scss+6
@@ -200,6 +200,12 @@ body.essay {
200 margin-top: 4rem;
200 margin-top: 4rem;
201 }
201 }
202
202
203+ blockquote {
204+ border-left: 1px solid black;
205+ padding-left: 2rem;
206+ font-style: italic;
207+ }
208+
203 img {
209 img {
204 display: block;
210 display: block;
205 }
211 }