-
Taking an overnight ferry to my home land. I expect to be on deck sipping a drink and working on a specification language to generate lower-level proof obligations for smart contract verification.
-
-
-
I read Notes on the Synthesis of Form before, which I loved the first half, the second half sounded like a formalization of the first and wasn’t that interesting.
Regarding “The Timeless Way” I like it, I haven’t read “A Pattern Language” yet, but I have the impression this one is better since it explains the concept of patterns and some examples without going to the formalization that “A Pattern Language” seems to go, which was the part I didn’t like about “Notes on the Synthesis of Form” :)
-
I enjoy the conceptual stuff too, although I’ve been reading Alexander’s later books and not the early ones. Pattern Language is interesting, but it’s mostly a collection of ~200 specific patterns for physical buildings.
I once read an book review that described The Timeless Way of Building as “underbaked,” A Pattern Language as “just right,” and The Nature of Order as “overbaked.” I’m inclined to agree, but overbaked is how I like it! Design patterns are already abstractions, but in TNOO Alexander really digs in and tries to determine what makes a good pattern. Here’s a thread from a couple years ago.
-
A Pattern Language gives you examples of patterns from the level of countries all the way down to rooms in your house. It’s filled with fascinating, humanistic reasons for each pattern. Some of my favorites:
- Have little hiding spaces in your house because kids like to hide in things.
- As a teen gets older, give them a space of their own, perhaps a room they can go into without coming through the rest of the house. That approach develops independence with age.
- There’s a really beautiful passage about building a marital bed and how it symbolizes coming together for the long future.
- It’s better to build cities where cars move slowly until they get to a fast highway. Not every little road needs to be super fast or wide. You actually end up losing little time in this situation, but you gain quieter and nicer spaces.
- Mixed residential and commercial development is the way to go. Downtowns are death because they are unused for half the day.
etc etc. I recommend getting it and reading a bit at a time, like a work of poetry.
-
Alexander wrote the following in his preface to Richard P. Gabriel’s book Patterns of Software:
In my life as an architect, I find that the single thing which inhibits young professionals, new students most severely, is their acceptance of standards that are too low. If I ask a student whether her design is as good as Chartres, she often smiles tolerantly at me as if to say, “Of course not, that isn’t what I am trying to do. . . . I could never do that.”
Then, I express my disagreement, and tell her: “That standard must be our standard. If you are going to be a builder, no other standard is worthwhile. That is what I expect of myself in my own buildings, and it is what I expect of my students.” Gradually, I show the students that they have a right to ask this of themselves, and must ask this of themselves. Once that level of standard is in their minds, they will be able to figure out, for themselves, how to do better, how to make something that is as profound as that.
Two things emanate from this changed standard. First, the work becomes more fun. It is deeper, it never gets tiresome or boring, because one can never really attain this standard. One’s work becomes a lifelong work, and one keeps trying and trying. So it becomes very fulfilling, to live in the light of a goal like this. But secondly, it does change what people are trying to do. It takes away from them the everyday, lower-level aspiration that is purely technical in nature, (and which we have come to accept) and replaces it with something deep, which will make a real difference to all of us that inhabit the earth.
I would like, in the spirit of Richard Gabriel’s searching questions, to ask the same of the software people who read this book. But at once I run into a problem. For a programmer, what is a comparable goal? What is the Chartres of programming? What task is at a high enough level to inspire people writing programs, to reach for the stars? Can you write a computer program on the same level as Fermat’s last theorem? Can you write a program which has the enabling power of Dr. Johnson’s dictionary? Can you write a program which has the productive power of Watt’s steam engine? Can you write a program which overcomes the gulf between the technical culture of our civilization, and which inserts itself into our human life as deeply as Eliot’s poems of the wasteland or Virginia Woolf’s “The Waves”?
-
-
Sounds like I will skip A Pattern Language and go with The Nature of Order then :)
Thanks!
-
-
-
-
-
I saw SAT solvers as academically interesting but didn’t think that they have many practical uses outside of other academic applications. … I have to say that modern SAT solvers are fast, neat and criminally underused by the industry.
Echoing a good comment on reddit: The author didn’t list any practical applications!!! How can you then say they are criminally underused?
The only one I know of is writing versioned dependency solver for a package manager (in the style of Debian’s apt). However, very few people need to write such code.
What are some other practical applications? I think they are all quite specialized and don’t come up in day-to-day programming. Happy to be proven wrong.
EDIT: I googled and I found some interesting use cases, but they’re indeed specialized. Not something I’ve done or seen my coworkers do:
https://www.quora.com/What-are-the-industrial-applications-of-all-SAT-solvers
http://www.carstensinz.de/talks/RISC-2005.pdf
I can think of a certain scheduling algorithm that might have used a SAT solver, but without details I can’t be sure.
-
-
A previous submission on SAT/SMT might help you answer that.
-
I’ve used Z3 to verify that a certain optimized bitvector operation is equivalent to the obvious implementation of the intended calculation.
Just typed up the two variants as functions in the SMT language with the bitvector primitives and asked Z3 for the satisfiability of f(x) != g(x) and rejoiced when it said “unsatisfiable.”
-
-
I’ll just post it here. :)
(define-sort Word () (_ BitVec 64)) (define-fun zero () Word (_ bv0 64)) ;; Signed addition can wrap if the signs of x and y are the same. ;; If both are positive and x + y < x, then overflow happened. ;; If both are negative and x + y > x, then underflow happened. (define-fun add-overflow-basic ((x Word) (y Word)) Bool (or (and (bvslt x zero) (bvslt y zero) (bvsgt (bvadd x y) x)) (and (bvsgt x zero) (bvsgt y zero) (bvslt (bvadd x y) x)))) ;; Here is a clever way to calculate the same truth value, ;; from _Hacker's Delight_, section 2.13. (define-fun add-overflow-clever ((x Word) (y Word)) Bool (bvslt (bvand (bvxor (bvadd x y) x) (bvxor (bvadd x y) y)) zero)) (set-option :pp.bv-literals false) (declare-const x Word) (declare-const y Word) (assert (not (= (add-overflow-basic x y) (add-overflow-clever x y)))) (check-sat) -
Here’s you an example of SMT solvers used for stuff like that. I added some more stuff in comments. You might also like some examples of Why3 code which is translated for use with multiple solvers. Why3 is main way people in verification community use solvers that I’m aware. WhyML is a nice, intermediate language.
-
-
-
-
I found this library (and its docs) interesting. They go over some practical examples.
-
-
-
-
Cory always scares me.
-
This was from 2012. Arguably, we’re already there. Tons of popular computers run signed bootloaders and won’t run arbitrary code. Popular OS vendors already pluck apps from their walled garden on the whims of freedom-optional sovereignties.
The civil war came and went and barely anyone took up arms. :(
-
It’s not like there won’t always be some subset of developer- and hacker-friendly computers available to us. Sure, iPhones are locked down but there are plenty of cheap Android phones which can be rooted, flashed with new firmware, etc. Same for laptops, there are still plenty to choose from where the TPM can be disabled or controlled.
Further, open ARM dev boards are getting both very powerful and very cheap. Ironically, it might even be appropriate to thank China and its dirt-cheap manufacturing industry for this freedom since without it, relatively small runs of these tiny complicated computers wouldn’t even be possible.
-
This is actually the danger. There will always be a need for machines for developers to use, but the risk is that these machines and the machines for everyone else (who the market seems to think don’t “need” actual control over their computers) will diverge increasingly. “Developer” machines will become more expensive, rarer, harder to find, and not something people who aren’t professional developers (e.g. kids) own.
We’re already seeing this happen to some extent. There are a large number of people who previously owned PCs but who now own only locked down smartphones and tablets (moreover, even if these devices aren’t locked down, they’re fundamentally oriented towards consumption, as I touched on here).
Losing the GPC war doesn’t mean non-locked-down machines disappearing; it simply means the percentage of people owning them will decline to a tiny percentage, and thus social irrelevance. The challenge is winning the GPC war for the general public, not just for developers. Apathy makes it feel like we’ve already lost.
-
-
Develop for, yes, within the bounds of what Apple deems permissible. But you can’t replace iOS and port Linux or Android to it because the hardware is very locked down. (Yes, you might be able to jailbreak the phone through some bug, until Apple patches it, anyway.)
Mind you, I’m not bemoaning the fact or chastising Apple or anything. They can do what they want. My original point was just that for every locked-down device that’s really a general-purpose computer inside, there are open alternatives and likely will be as long as there is a market for them and a way to cheaply manufacture them.
-
Absolutely! Even more impressive is that with Android, Google has made such a (mostly) open architecture into a mass market success.
However it’s interesting to note that on that very architecture, if you buy an average Android phone, it’s locked down with vendorware such that in order to install what you want you’ll likely have to wipe the entire ecosystem off the phone and substitute an OSS distribution.
I get that the point here is that you CAN, but again, most users don’t want the wild wild west. Because, fundamentally, they don’t care. They want devices (and computers) that work.
-
Google has made such a (mostly) open architecture into a mass market success.
Uh, I used to say that until I looked at the history and the present. I think it’s more accurate that they made a proprietary platform on an open core a huge success by tying it into their existing, huge market. They’ve been making it more proprietary over time, too. So, maybe that’s giving them too much credit. I’ll still credit them with their strategy doing more good for open-source or user-controlled phones than their major competitors. I think it’s just a side effect of GPL and them being too cheap to rewrite core at this point, though.
-
-
-
-
This is not completely true. There are some features you can’t use without an Apple developer account which costs $100/yr. One of those features is NetworkExtension.
-
-
-
-
-
Over half a million people or 2 out of 100 Americans died in the Civil War. There was little innocent folks in general public could do to prevent it or minimize losses Personally, I found his “civil war” to be less scary. The public can stamp these problems out if they merely care.
That they consistently are apathetic is what scares me.
-
Agreed 100%.
I have no idea what to do. The best solution I think is education. I’m a software engineer. Not the best one ever, but I try my best. I try to be a good computing citizen, using free software whenever possible. Only once did I meet a coworker who shared my values about free software and not putting so much trust in our computing devices - the other 99% of the time, my fellow devs think I’m crazy for giving a damn.
Let alone what people without technical backgrounds give a damn about this stuff. If citizens cared and demanded freedom in their software, that would position society much better to handle “software eating the world”.
-
The freedoms guaranteed by free software were always deeply abstruse and inaccessible for laypeople.
Your GNOME desktop can be 100% GPL and it will still be nearly impossible for you to even try to change anything about it; even locating the source code for any given feature is hard.
That’s not to say free software isn’t important or beneficial—it’s a crucial and historical movement. But it’s sad that it takes so much expertise to alter and recompile a typical program.
GNU started with an ambition to have a user desktop system that’s extensible and hackable via Lisp or Scheme. That didn’t really happen, outside of Emacs.
-
Your GNOME desktop can be 100% GPL and it will still be nearly impossible for you to even try to change anything about it; even locating the source code for any given feature is hard.
I tried to see how true that is with a random feature. I picked brightness setting in the system status area. Finding the source for this was not so hard, it took me a few minutes (turns out it is JavaScript). Of course it would have been better if there was something similar to browser developer tools somewhere.
Modifying it would probably be harder since I can’t find a file called
brightness.json my machine. I suppose they pack the JavaScript code somehow…About 10 years ago (before it switched to ELF) I used Minix3 as my main OS for about a year. It was very hackable. We did something called “tracking current” (which apparently is still possible): the source code for the whole OS was on the disk and it was easy to modify and recompile everything. I wish more systems worked like this.
-
-
-
-
-
-
-
There is one aspect where Ed maybe has an actual advantage: It keeps you in write mode and discourages editing. I will consider using Ed for journalling where I currently use vim.
-
There is one aspect where Ed maybe has an actual advantage: It keeps you in write mode and discourages editing.
cat > $filenamewill do that, too, but withedI can switch back to command mode, save what I’ve done so far, and then continue by returning to append mode.Though I could probably do the same with
cat >> $filename, but I’m afraid I’d forget that I need to type > twice to append and end up overwriting the file. :) -
-
-
-
Thanks for this amazing project!
If I may, I’d like to gently complain about this sentence:
Provably correct code is code that you can totally guarantee does what you say it does.
Thinking about total guarantees in this way confused me about proving code for a long time. Whenever I saw a “proven” piece of software, I could immediately think of several possible ways for it to nevertheless be wrong, so it was unclear how the “proof” was qualitatively different from other verification strategies.
Maybe a more accurate description could be:
Provably correct code is code that has been rigorously shown to implement a thorough specification using proof techniques from mathematical and logical praxis.
-
Yeah, I’m against the use of word guarantee or anything absolute like that. It hurt the formal methods field in the past when they were overpromising. Maybe something like, “Provably correct code is mathematically-proven to implement its intended behavior. If the specification is correct, code built this way usually has few to no errors in practice.”
Something along those lines. Maybe even with a link to CompCert’s testing results or something like that to illustrate the point.
-
Correctness is a relation between the input and output of a program. We say a program is correct if for every possible input, an execution of the program eventually results in a termination with the expected output.
The correctness relation is called functional if for every input only a single output is related. That is, each input uniquely determines an output.
Not all correctness relations have a correct program. An input-output relation for which no correct program exists is called undecidable. On the other hand, some correctness relations have multiple correct programs.
Typically, a programming language itself is already a specification language that allows one to establish an input-output relation in a rigorous manner. Sometimes one wishes to give a functional/relational specification before implementing a program, typically written down using mathematical notation.
Recent tools allow us to express functional/relational specifications on the computer too:
- “Abstract spectification:” To specify the input output relation in a more expressive logic. This logic might not have a direct computational or algorithmic interpretation, and this logic typically has many undecidable properties,
- “Concrete Implementation:” The specification in a target programming language. We also need a termination proof of the program.
- “Refinement:” showing that each input-output pair in the concrete implementation is also in the abstract specification (soundness), and each input-output pair in the abstract specification is also included in the input-output pair of the concrete implementation (completeness).
This is, of course, a simplification. Typically, the system one wishes to formalize is not functional, and thus requires more effort in abstract specification and refinement.
The words “rigorous” and “thorough” are not needed.
-
There’s a difference between establishing all that in math and it actually being true for the real code. It requires your specification to be correct, any specs/logics it depends on, the proofs, the checker, usually a parser, usually some I/O, the hardware, and so on. In this case, some of them needed automated solvers to be correct that are pretty complicated. I’m no sure that all have witness certificates or whatever they’re called yet. To be fair to proof engineers, many of them mention all of the above in their papers in the section describing assumptions and/or the TCB.
So, mbrock’s point that calling it a guarantee is too much seems to stand. I mean, even the seL4 people didn’t call it a total guarantee. They said the code should follow the spec assuming (long list here) isn’t wrong or broken.
-
I agree with your points. A proof is as much worth as you want it to be. See the DeepSpec project which tries to obtain proofs for a pragmatic computer: hardware specifications, OS specifications, prover specifications et cetera. However, this still not guarantees anything absolute.
My point is still that “Rigorously shown:” is vague. When is a method that shows correctness rigorous, when is it not? “Thorough specification:” is vague. When is a specification thorough, when not? Both are matters of trust, it seems to me.
“But there is a difference between showing that in math and it really being true for code.” Well, if one mathematically deduces a property of some code, and it turns out to be really false, one should start to doubt the foundations or mechanism by which the deduction took place. In principle, any deduction should be true for the real code.
Although in some logics, not all true properties can be deduced (incompleteness), it does not mean that we should accept logics in which false properties can be deduced (unsoundness).
Or did I misunderstand what you mean by “the real code”?
-
“My point is still that “Rigorously shown:” is vague”
Ok. That’s a decent point. It is kind of vague. It does have a subjective meaning that a lot of people already understand. They think that a “rigorous” analysis, testing, or whatever phase means piles of effort was put in vs a non-rigorous approach. They expect to get significantly more results or less problems. The fact that people rarely use that word for software QA might make that perception sink in even more.
I think I mainly keep using it for the psychological impact on people that might not understand the formal terminology well. I could tell them it relates to the specification. Yet, they might think UML when I say that. So, personally, I use a mix of precise terms from the field and terms that seem to convey understanding to those outside of it. I have no proof this term is better: by all means experiment to see if it works in your conversations or find a better way to say it. Talking rigorous vs typical QA has just worked for me. From there, I might say low, medium, or high rigor, confidence, and so on. Although the field is called assurance, I’m thinking of ditching that word, too, since confidence clicks in more people’s heads. I’ve been seeing some people talking about “high-confidence” software or techniques that “increase confidence that software works as intended.” Robustness and resilience are the other two terms many are using.
-
-
-
-
Clean code, pure code, agile code, pragmatic code, elegant code, simple code, awesome code, …
Let’s talk more about the big ball of mud.
-
ianloic
4 months ago
|
link
| on:
Why you should verify the tokens you own: A deep dive into two vulnerable ERC20 contracts
Amazing. I kind of can’t believe they built integer overflow into the etherium vm. But then I also totally can.
Do the authors of those “contracts” have enough political clout to get a hard fork that patches & reverts or are they outside of the eth oligopoly?
-
-
If humans are going to be reading, supporting, and re-writing code, I don’t see why we’d want to eschew one’s strongest language, say, English, in favor of one that reads like hieroglyphics.
Look at what humans already do in domains that require precision, as programming does. “reads like hieroglyphics” is a fair description of a lot of mathematical notation, yet mathematicians have long preferred symbology to English - if you think programmers shouldn’t then you should be able to explain why mathematicians do. Lawyers write “English” but in a famously stilted style, full of clunky standardized constructions, to the point that it’s sometimes considered a distinct dialect (“legalese”) and one could reasonably ask whether a variant that used a symbol-based language would be more readable. And of course it bears remembering that the most popular human first language is notated not with alphabetics but with ideograms where distinct concepts generally have their own distinct symbols.
Even within programming, humans who are explaining an algorithm to other humans tend not to use English but rather a mix of “pseudocode” (sometimes likened to Python) and mathematical notation.
Erlang is notorious for being ‘ugly,’ but I wonder what that’s all about. Truly. I like to think most my Erlang code is composed of English sentences, lumped together into paragraphs, and contained in solitary modules. It’s familiar, unsurprising, and quite beautiful when one’s naming is in top form.
Really? Most languages allow sensible plain English names for concepts. The part of Erlang that’s notoriously ugly - and the part that makes it read very unlike English - is its unusual punctuation style. If the author really finds Erlang English-like to read, I can only assume this is because they’re much more familiar with Erlang than other languages, rather than the language being objectively more English-like than, say, Python or Java.
-
Erlang’s punctuation style is more like English than most C-likes out there. Let’s take this statement:
I will need a few items on my trip: if it’s sunny, sunscreen, water, and a hat; if it’s rainy, an umbrella, and a raincoat; if it’s windy, a kite, and a shirt.
In a C-style language (here, go) it might look something like
switch weather.Now() { case weather.Sunny: sunscreen() water() hat() case weather.Rainy: umbrella() raincoat() case weather.Windy: kite() shirt() }In Erlang it could just be:
case weather() of sunny -> sunscreen(), water(), hat(); rainy -> umbrella(), raincoat(); windy -> kite(), shirt() end.You even get to keep the
,for enumeration/sequences,;for alternative clauses, and.for full stops!-
That example is a little misleading. In C and C++ it could be written like this, which arguably reads more like English than either Erlang or Go:
if ( weather() == Sunny ) { sunscreen(), water(), hat(); } else if ( weather() == Rainy ) { umbrella(), raincoat(); } else if ( weather() == Windy ) { kite(), shirt(); } -
-
-
Mathematicians use a seamless hybrid of prose and formula:
For every v ∈ V, there exists w ∈ V such that v + w = 0.
Similarly in code, some parts are more like formulae, some are more like prose, and some are more like tables or figures… and it’s interesting to consider separate syntaxes for these different types of definitions.
Have a look at the Inform 7 manual’s section on equations, for an example. Here is a (formal, compiling, working) definition of what should happen when the player types
push cannonball(I’ve used bullet lists in Markdown to get indentation without monospace):-
Equation - Newton’s Second Law
- F=ma
-
where F is a force, m is a mass, a is an acceleration.
-
Equation - Principle of Conservation of Energy
- mgh = mv^2/2
-
where m is a mass, h is a length, v is a velocity, and g is the acceleration due to gravity.
-
Equation - Galilean Equation for a Falling Body
- v = gt
-
where g is the acceleration due to gravity, v is a velocity, and t is an elapsed time.
-
Instead of pushing the cannon ball:
- let the falling body be the cannon ball;
- let m be the mass of the falling body;
- let h be 1.2m;
- let F be given by Newton’s Second Law where a is the acceleration due to gravity;
- let v be given by the Principle of Conservation of Energy;
- let t be given by the Galilean Equation for a Falling Body;
- say “You push [the falling body] off the bench, at a height of [h], and, subject to a downward force of [F], it falls. [t to the nearest 0.01s] later, this mass of [m] hits the floor at [v].”;
- now the falling body is in the location.
(Yes, the Inform 7 compiler will solve equations for you. Why aren’t normal programming languages capable of this kind of high school math? Are we living in some kind of weird bubble?)
-
Why aren’t normal programming languages capable of this kind of high school math?
They are. Inform 7 uses English words as syntax, but otherwise is a normal programming language. Why do you think this can’t be solved in, say, Python?
-
Of course it can be solved in any general purpose programming language, but none of them feature dimensional analysis or algebraic equation solving out of the box in a convenient and natural way… yet Inform 7 does, oddly.
I find this interesting because that stuff would seem to be the most obvious use case for computing machines from, like, a 1930s perspective.
-
Ah, my apologies for completely misunderstanding what you said.
I completely agree. Python (and maybe Basic?) are close, but even then they fall dramatically short of “language as code” as Inform 7 does. I wonder what keeps Inform 7 from becoming a more general purpose programming language?
-
-
-
-
Also, English isn’t everyone’s strongest language. As natural languages go, it’s pretty complex and inconsistent. If you want your code to be understood by people who are more familiar and comfortable with other natural languages, then your own familiarity with English isn’t necessarily such an advantage in writing code.
-
-
-
CGI is beautiful and perfect and it is sad how neglected it is nowadays.
-
CGI is pretty awesome, and I’ve always wanted to find a nice way of using Python with it
Unfortunately there’s a bit of an awkwardness when trying to pair CGI with something like Django. Having to set up the environment over and over. Also there’s the basic issues of URL routing being coupled with files…
I’m sure there’s some nice style of dealing with this, but I haven’t found it yet.
-
-
I think a lot of those weren’t even CGI per se, but just that perl and php (and other interpreted languages) have nasty startup costs. I often do traditional CGI programs in the natively-compiled D language and while it doesn’t win any benchmarks, it is also good enough for a LOT of things - and very reliable, thanks to process isolation.
-
-
I’ve also been playing around with Go’s net/http/cgi package, which is quite nice, since it uses the same backend as the regular http, as well as the fcgi package. One can even bundle them together into one binary, that chooses what to done depending on the file name (example for a mini lobste.rs clone I wrote a while ago).
And from my experience, which wasn’t quite the worst, it was quite enough. I sometimes have the feeling that modern web frameworks have created a fear of these more simple and often sufficient solutions (for smaller to mid-size usecases), to promote their own projects - unrightfully.
-
Yeah, the library I wrote for D also uses the same interface for cgi, fcgi, scgi, and http (both pre-fork processes to provide some segfault isolation as well as simple multiplexing, and one-thread-per-connection primarily for compatibility on non-Linux systems where fork doesn’t work the same way) implementations, so swapping out is often as simple as a recompile.
I don’t even think CGI is really dead, but rather just slightly extended or wrapped by everyone individually. Python’s WSGI and Ruby’s rack show their cgi heritage and compatibility, etc.
-
-
-
-
-
Yogthos
4 months ago
|
link
| on:
Programming Languages as Operating Systems (or Revenge of the Son of the Lisp Machine)
It’s really unfortunate that the idea of a live coding remains niche, and most programmers haven’t had exposure to this style of development. Working in an environment where you can inspect and change any aspect of the system at runtime is the most satisfying coding experience in my opinion.
-
Coding hackers tell me they want to understand, change, and improve on anything they can get their hands on. The live coding systems let them do that to their whole, running system. It just seems like the two are a natural fit. It makes it so much stranger to me to see such people use tools that limit them so much.
-
-
I would also add Erlang to that list, but that might be controversial.
-
-
The tracing capabilities and the ability what process is doing what and which messages are being received is quite impressive.
-
-
Yeah, I don’t know if it fits since I don’t use it. I will say that making distributed, concurrent systems easier and more robust by design with ability to update running systems makes it pretty close to the idea. It’s kind of in its own category in my mind where the LISP’s were focused on max flexibility where things like Erlang or Ada are focused on max reliability. Erlang improved on things like Ada in its category by being more high-level, distributed, the updates, etc.
Now, it might be interesting to combine the two. I swore someone… (checks bookmarks) Oh yeah, it was LISP-Flavored Erlang. I can’t evaluate further about whether it truly has benefits of typical LISP workflow and Erlang since I don’t know Erlang or LFE. Looked really awesome conceptually when I found it. Anyone else chime in?
-
-
-
Pervasively dynamic environments are a two-edged sword: with great power comes great responsibility. It’s trivial to render a Smalltalk image completely unusable with something as simple as
false become: true. PicoLisp has similar capabilities. Most Forths do too. There’s something to be said for isolating and stabilizing some basic parts of the system: such limitations give us a margin of safety!
-
-
-
I’ve had a lot of fun with Haskell’s
bricklibrary, which makes terminal user interface development nice and easy.
-
mbrock
4 months ago
|
link
| on:
What programming languages have been designed to reduce naming things?
In Haskell you can just name your variables
x,f,m,a, and so on, provided you’re writing at a sufficiently high level of polymorphism, so you don’t usually have to come up with names likehandlerFactoryManager.Agda is even better because you tend to use all kinds of Greek letters, Unicode dingbats, and box-drawing characters.
-
I’m working on automated testing of a smart contract system that will handle many millions of dollars worth of tokens on the Ethereum main net. This is in addition to other formal methods our team is using.
The approach I’ve chosen is to write an exact model of the system in Haskell, which also serves as a kind of specification, along with whole-state invariants, and then running that model simultaneously with the real bytecode with randomly generated action sequences as input, verifying that the implementation matches the model and that all extra invariants hold on the model state.
In addition, I’m also doing a simple kind of mutation testing using the same test suite, where I make random alterations to the bytecode—e.g., switching an
LTto aGTor frobbing a constant value—and verify that the test suite then fails.-
That should work pretty well. It’s similar to what I’ve seen a lot of groups do with stuff like matching functional specs to imperative or imperative code to assembly. For anyone interested in these things, my favorite one was still this project that used ASM’s with great productivity and model size. ASM’s advantage over Haskell is that surveys showed they’re one of easiest formalisms to understand since they’re basically abstracted FSM’s. The simple programs, VM’s, and actual assembly are also usually FSM’s. So, they fit together really well.
-
-
Smart contracts aren’t possible on Cardano yet—it’s in the research phase, as far as I know. They have a very interesting team and I’m sure the platform will become amazing, but for now, Ethereum is the only viable platform for us. (It’s “worse is better” all over again.) The first version of our smart contract system is already live today, and we’re aiming to deploy the next version this summer.
We’ve developed an Ethereum VM in Haskell (
hevm) which is already being used as a library to support property-based testing (in the Echidna system by Trail of Bits, and our own system).And despite being huge fans of pure functional programming, we think it’s possible to write correct—even provably correct contracts—for the Ethereum virtual machine. (There’s a lot of misunderstandings out there, like “you can only prove the correctness of functional programs” and “Turing-complete programs cannot be proven correct,” and so on.)
-
-
-
codemac
4 months ago
|
link
| on:
Formal Specification and Verification of Interactive Systems with Plasticity for Nuclear Plants
I always love thesis dedications. It reminds me how much human life goes into each of these papers I tuck into ~/docs/pdf.
I dedicate this thesis to you, NH. Your continuous support and love throughout the writing of this thesis and also within my own life helped me in more ways than you probably realize. In the vastness of space and immensity of time, it is my joy to spend a planet and an epoch with you.
-
I remember reading one dedication where it was obvious that the author was not pleased with the support of his advisors or something. Basically they said “my parents are awesome, my wife’s wonderful. My advisors were Bob, Sue, and Joe.”
-
And don’t forget Olin Shivers’ acknowledgements section for Scsh (1994).
Who should I thank? My so-called “colleagues,” who laugh at me behind my back, all the while becoming famous on my work? My worthless graduate students, whose computer skills appear to be limited to downloading bitmaps off of netnews? My parents, who are still waiting for me to quit “fooling around with computers,” go to med school, and become a radiologist? My department chairman, a manager who gives one new insight into and sympathy for disgruntled postal workers?
My God, no one could blame me – no one! – if I went off the edge and just lost it completely one day. I couldn’t get through the day as it is without the Prozac and Jack Daniels I keep on the shelf, behind my Tops-20 JSYS manuals. I start getting the shakes real bad around 10am, right before my advisor meetings. A 10 oz. Jack ‘n Zac helps me get through the meetings without one of my students winding up with his severed head in a bowling-ball bag. They look at me funny; they think I twitch a lot. I’m not twitching. I’m controlling my impulse to snag my 9mm Sig-Sauer out from my day-pack and make a few strong points about the quality of undergraduate education in Amerika.
If I thought anyone cared, if I thought anyone would even be reading this, I’d probably make an effort to keep up appearances until the last possible moment. But no one does, and no one will. So I can pretty much say exactly what I think.
Oh, yes, the acknowledgements. I think not. I did it. I did it all, by myself.
-
-
-
Unless I am misunderstanding “Brutalism”, shouldn’t a “brutalist web site” be something like a no- or minimal-css web page? The examples the article gives, while pretty in their own right, don’t appear (to me) to go counter to much of everyday web-design one tends to see.
-
That’s my understanding, too. My touchstones for web Brutalism are this motherfucking website and this other motherfucker.
-
There’s another school that considers the Instragram iOS app as an example of brutalism. Other examples:
Brutalist websites
Brutalism in UXI consider the two sites that you linked to more an example of design minimalism (only using as much as you need), as opposed to the minimalism of information that seems to typify “modern” design today.
I’d also be curious if y’all would consider something like my wiki as an example of brutalism
-
I’d say it’s pretty brutalist. It probably wasn’t designed or implemented with accessibility in mind. :)
-
-
-
-
I would imagine that to draw a useful analog to architecture, we have to imagine what it is we’re saving or optimizing for under a digital brutalism (in the same way that architectural brutalism is cheaper, easier, faster, less specialized, in addition to its aesthetic impact). As a programmer, I would imagine therefore that digital brutalism would have to at least partially be motivated by a desire for simplicity in construction: avoiding a reliance external resources that might not be available, avoiding a reliance on technologies or techniques that require specialization, avoiding techniques that require complexity in order to be correct (in favor of technologies that, while maybe less rich, can be correct more simply), and optimizing resource usage for browser speed and compatibility.
I think it’s perfectly fair to associate the above motivations with a particular aesthetic if they happen to be accompanied by one (after all, when I think about architectural brutalism I don’t think about the equipment, specialized or un-, that was used to construct it). But to say anything useful or interesting with term, it can’t just be the way they look.
-
But to say anything useful or interesting with term, it can’t just be the way they look.
Isn’t look (legibility) in print/web design fundamental? If we’re talking about a brutalist web design, it’s certainly not brutalist because the author used tables for layout, though that might contribute to a look that has hard edges (defining sections/compartments, etc)–an element often associated with brutalism.
-
Legibility and aesthetic are not the same, though. As I said above, it’s not that aesthetics are irrelevant; but using modern whizbang web design and tech, and just replacing your full-screen white-people-typing-together background video with graphics and video of a different aesthetic, is just another flavor of the status quo.
-
Legibility and aesthetic are not the same, though.
I agree with this.
and just replacing your full-screen white-people-typing-together background video with graphics and video of a different aesthetic
What I think you’re saying is that Brutalism is a philosophy that can’t simply be replicated by copying an aesthetic. Is that right?
-
-
-
-
-
Wikipedia has a nice passage which I think can be applied in spirit to websites:
Brutalist buildings are usually formed with repeated modular elements forming masses representing specific functional zones, distinctly articulated and grouped together into a unified whole. Concrete is used for its raw and unpretentious honesty, contrasting dramatically with the highly refined and ornamented buildings constructed in the elite Beaux-Arts style. Surfaces of cast concrete are made to reveal the basic nature of its construction, revealing the texture of the wooden planks used for the in-situ casting forms. Brutalist building materials also include brick, glass, steel, rough-hewn stone, and gabions. Conversely, not all buildings exhibiting an exposed concrete exterior can be considered Brutalist, and may belong to one of a range of architectural styles including Constructivism, International Style, Expressionism, Postmodernism, and Deconstructivism.
Another common theme in Brutalist designs is the exposure of the building’s functions—ranging from their structure and services to their human use—in the exterior of the building.
So don’t do elaborate styling, expose how the site was built, and organize the site into functional zones in ways visible to the user. A thoughtful version of non-CSS, non-Javascript, image-light design might be the best Web “version” of Brutalism, with visual grouping being the only organization. Getting people to give up CSS and Javascript might be a bit much, but in terms of basic construction, HTML is the equivalent of concrete (the “raw structural members” of the Web site) and Brutalism is very much about not hiding or ornamenting that.
-
Getting people to give up CSS and Javascript might be a bit much, but in terms of basic construction, HTML is the equivalent of concrete (the “raw structural members” of the Web site) and Brutalism is very much about not hiding or ornamenting that.
I have no trouble giving up JavaScript. I’d prefer to use mostly semantic HTML5, with just enough CSS to make the text more readable (because browser defaults are trash).
-
Great excerpt and follow up. I think you can keep CSS so long as what it’s doing is (a) visible in source behind the scenes, maybe even removable and (b) keeps the fundamental structure of the site or page. It might even give it the structure.
-
-
Maybe GeoCities was brutalist? http://oneterabyteofkilobyteage.tumblr.com/
-
The Classic Geocities, with all of its animated GIFs and background images and using images as dividers, is too ornamented to be Brutalist. It’s best described as Vernacular, which Wikipedia describes as:
Vernacular architecture is an architectural style that is designed based on local needs, availability of construction materials and reflecting local traditions. At least originally, vernacular architecture did not use formally-schooled architects, but relied on the design skills and tradition of local builders. However, since the late 19th century many professional architects have worked in this style.
The Geocities Vernacular was definitely the “architecture from people who weren’t architects” Vernacular.
In fact, the Terabyte Of The Kilobyte Age describes Geocities as Vernacular:
http://blog.geocities.institute/archives/5983
More to the point, Vernacular design is bottom-up unplanned design, with no large-scale goals in mind, whereas Brutalism is top-down planned design, and capable of designing in the large.
-
-
-
That would be in line with architectural brutalism, but the term came out of critiques of architectural brutalism (which basically came down to “it’s ugly because it breaks convention in non-decorative ways”). “Web brut” has been used as an insult for longer than its current (3-4 year) rehabilitation.
I think both senses are useful for different reasons. Web brutalism in the sense of avoiding bloated web standards that necessitate bloated browsers is important for usability and for minimizing waste, while web brutalism in the sense of rejecting faux-minimalist aesthetics in favor of direct & straightforward mapping of form to function is important as a UX concern. (I’ve argued for the latter in https://lobste.rs/s/cyopoi/against_ui_standardization and the former in https://hackernoon.com/on-the-web-size-matters-e52ac0f5fdbe and https://hackernoon.com/an-alternate-web-design-style-guide-1aae8d0b5df5)
-
Regarding your hackernoon article where you say
Use only the following tags: a, b, body, br, center, h1, head, i, li, ol, p, table, th, title, td, tr, ul. All other tags are unnecessary distractions. If, for some reason, you must include images, the img and align tags are also suitable.
what would your thoughts be on directly hostilng markdown, probably without literal html, instead of the “more powerful” full-html standards and deviations? Maybe protocols like Gopher could serve as a base for this?
-
I consider hosting markdown marginally more reasonable than hosting html, but to be honest I don’t think we, as writers, should be controlling how the text is formatted except in the rare cases when the formatting is truly necessary and part of the point (like, if we’re writing concrete poetry or something).
In other words, something like gophermaps-as-document-format seems ideal: we get jump links, but literally nothing else.
The alternate web design style guide, despite apparently looking pretty radical to a lot of web devs, was very much a compromise – in the vein of “oh, if we MUST have web standards at all, at least ditch everything other than HTML 1.0!”
-
-
-
-
I started today on my ideal personal day planning tool. It’s a very simple browser app where I can create a number of blocks for the day—like a queue of named pomodoros with an implied flexible break between them.
I’m learning to write good specifications and enjoying playing with TLA+ and watching talks by Leslie Lamport and Ron Pressler.
Now I’m going to a meeting for a local obscure political magazine for which I have ended up as the WordPress guy.
-
Made a new release and a brand new readme for https://github.com/dapphub/seth — our command-line tool for Ethereum.
I also started playing around with “planning” — using old school STRIPS-style “good old fashioned AI” planners, as well as Ceptre & Celf to do planning in the form of linear logic solving — as part of some hobby research into user interfaces based on automatic plans.
Finally I’m continuing thinking about smart contract language design.
-
Two approaches I found interesting when studying classic AI were Procedural Reasoning System and Firby’s Reactive, Action Packages. You might enjoy making some knockoff of them.
-
-
I don’t know if that well-understood phenomenon is interesting or depressing given I was one with high hopes for it all. The job was just way harder than people thought. Our brains are really just amazing. :)
Well, that’s why it all got defunct. The availability part might have come from how so much was done in commercial/defunct LISP’s, Prolog’s, Poplog’s, and other obscure stuff on odd machines or OS’s. Then, just older stuff being hard to get a hold of in general. They used weirder tooling than most, though.
-
I’ve understood that there is an annual competition for automated planning.
http://icaps-conference.org/index.php/Main/Competitions
All the software seems pretty obscure, though!
There are several numbered major versions of the PDDL action language, but it’s nearly impossible to find implementations of any of them…
With linear logic programming, it seems like quite a well-developed research topic, but the only implementations I’ve found are Celf and Ceptre, neither of which are really polished (and Celf’s last commit was years ago)…
Actually I’ve read some on the deep critique of symbolic intelligence, especially in Hubert Dreyfus’s Being-in-the-world, which is philosophically fascinating and seems accurate. But automated logical reasoning, even though it can’t “come alive”, still seems like a primary reason to even have computers.
At a summer school of GF (Grammatical Framework) last year, I got the impression that formal grammar models is still very much an active research topic. Hybridizing it with neural models seems like the frontier. I assume there’s some similar hybrid program in automated logic. Grammar, semantics, and logic are so intertwined anyway…
-
It’s really interesting you said the competition because that was in me comment preediting to cut size. I originally wrote another trend in AI was that narrowly-focused AI tech that got really great stopped being called AI any more. The examples I had were computer vision and planning noting that the new sub-fields had their own conferences. They get obscure, too, when that happens.
I recently saw the planners in conferences last year looking up where the field was at for a scheduling use-case. We have so many that perform well. Scheduling, esp timetabling, is such a big problem across the US you’d think the algorithms or FOSS solutions would get more attention.
So, the obscurity on AI side makes sense to me given AI Winter and Narrow AI Is Not AI Effect. The part that’s strange for me is operations side not utilizing them effectively.
One more thing: the machine/deep learning side has a momentum going so strong it’s redefined AI to mean that in minds of a lot of people. Quite a few AI majors I met at ML-focuses places didnt think traditional AI was even being developed any more. They never saw it. Silo effect from drowning out.
-
-
-
-
-
-
Longtime user of StumpWM here. I really enjoy using it; it’s very nice to be able to easily extend my window manager while it’s running, and to have a complete Common Lisp environment always available. Highly recommended.
-
I’ve been using i3 for years but recently came back to StumpWM because Common Lisp is my favorite language. Going from i3 to StumpWM is a small step (there’s some advantages in both of them compared to the other) and I haven’t run into major issues the last couple of weeks. It is also stable.
So, recommended as well!
-
-
My only problem is that [StumpWM] only supports bitmap fonts …
Luckily, that’s not true. I’m using TrueType with StumpWM just fine.
Just get ttf-fonts & then throw this at the top of your config:
(ql:quickload '(#:clx-truetype #:ttf-fonts)) (set-font (make-instance 'xft:font :family "Source Code Pro Semibold" :subfamily "regular" :size 12))(changing the args as you like — I find that Source Code Pro is an awesome font)
-
-
-
I don’t know if language choice has anything to do with it, but the fact remains: the service is now dead. ;)
I agree in 2012 the state of Python3 support was a valid concern, and I have to admit actively discouraging people from learning it at the time, but luckily that part hasn’t aged well. I still want better FP support in Python of course.
My biggest problem with Common Lisp is that it’s a Lisp-2. Why would anyone want different namespaces for functions and other bindings in an ostensibly functional language?
According to this site, one of the arguments was “backwards compatibility”:
which I don’t find that convincing, since there were plenty of lisps using dynamic scoping, despite CL using lexical scopes. But I agree, things like these together with, frankly wierd function names always annoy me. I’d guess that in the end, CL shouldn’t be seen as a functional language, since Lisp wasn’t even originally conceived as functional language.
There’s a page which I can’t find now which makes the case that the term “functional programming language” evolves over time to mean “the most functional programming language which currently exists”, so different features rotate in and out of defining what it effectively means to be a functional programming language.
(I’d add that each generation has a different boogeyman idea, an idea which the Average Programmer regards as being “too complex” and which others write blog posts or the local equivalent to explain.)
The first generation was when Algol introduced recursion. Recursion is also the boogeyman idea of this era.
The second generation begins with “mature” Lisp (that is, Lisp implementations like MACLISP and Lisp Machine Lisps, not LISP 1.5) and, later, Scheme, where the defining feature is first-class functions and closures, and the boogeyman idea is Scheme’s continuations. Common features are strong dynamic typing and a universal feature is garbage collection. The new-school scripting languages (Perl, Python, Ruby) are languages of this type with object systems bolted on, and Java’s getting there, slowly.
(Some pre-Common Lisp Lisps didn’t have closures. They had the upwards funarg problem, instead.)
The third generation is ML and everything after, including OCaml and Haskell. Now, functional programming includes strong, static type systems with algebraic types, Hindley-Milner type inference, and, at a syntactic level, pattern-matching as flow control. The boogeyman idea is monads, and, more specifically, requiring the use of monads to mark out side-effecting code, as Haskell does.
The underlying point is that “Functional programming is whatever your language of choice doesn’t have yet”: Recursion is now universal. It wasn’t when FORTRAN IV was “your language of choice” for a lot of programmers. Strong dynamic typing and garbage collection aren’t universal, but they’re not weird and wacky ideas only long-haired MIT AI Lab types can make sense of. Marking your side-effecting code in a machine-readable way is still weird and wacky… for now.
I wonder why backwards compatibility was a concern if CL could not run any of that old code unmodified. Ot could it?
Common Lisp could be implemented in terms of the Old Lisps with a library of functions and macros. That’s the kind of compatibility they were after.
I’m pretty sure backwards compatibility with most existing implementations was exactly the goal. I’ve heard you can run early Lisp programs on CL with minimal modifications to this day, but I’ve never tried it myself.
It might be slightly easier to write tooling when you know what’s a function and what’s a variable.
On the other hand, if you use a Lisp-2 in functional style (which poorly suits Common Lisp), you still have the problem of full analysis between the boundary of namespaces + awkward syntax. It looks like Common Lisp is meant to be used in imperative style, without juggling functions as values.
Yeah, I guess it’s my expecation that the language is supposed to be functional that makes lisp-2 look so disappointing for me. It technically has everything for FP to work, so I feel cheated. ;)
Does it really pose a significant problem?