1. 4

TLA+, IMHO should be used by everyone building large complex software. It’s the only clear way to think about such systems.

1. 8

I really like the idea of extending HTML to support many common UI patterns that currently need JS. In a sense this is nothing new. We have built in calendar picker, button hovers and form validation all of which requires JS before they where included in HTML or CSS.

This would be the next logical step, allow HTML to make HTTP requests and replace small parts of the page.

1. 3

Precisely! Stuff like routing, data binding & http requests should be doable out of the box.

1. 1

I watched this course last year. I couldn’t believe how short and concise this course was.

I effortlessly learnt alot. I wish all math topics had such an approach.

1. 8

To say nothing of Ada Lovelace - a true genius.

1. 5

This post is pretty interesting because it removes a lot of the doubt and mystery about her contributions to CS - she even wrote the first bug!

1. 1

Did Ada Lovelace have any books or essays? I Would like to have a comprehensive grasp of her work.

1. 6

Her sole published work was her report on Babbage’s engine. At the time it was still difficult for women to be accepted as scientists and interpreting men’s work was one of the few paths open; Ada’s tutor Mary Somerville was (jointly) the first woman ever accepted into the Royal Astronomical Society, and she had made her name by translating Laplace’s work from French into English. (In the previous century Émilie du Châtelet had followed a similar path translating Newton from English into French.) George Boole who was Ada’s contemporary — they were born in the same year — had a daughter who was the first ever female professor of chemistry: it was still early times for women in science… Ada herself was unable to access even the Royal Society’s library, and that with her husband being a Fellow. (The RS would not accept women until 1945!)

As for what happened after publishing her report, she had a falling-out with Babbage and, while they eventually reconciled, they never properly worked together again. She lived for less than a decade after her article was published and spent many of those years sick. A quote from “The Lovelace–De Morgan mathematical correspondence: A critical re-appraisal”:

It is the contrast between the mathematics that she actually wrote and her mathematical potential that has fuelled much of the debates regarding Lovelace’s mathematical ability; for despite De Morgan’s prediction that she would “get beyond the present bounds of knowledge”, we have no evidence that she created original mathematics in either published or unpublished form. The reasons for this await further research, but were probably a combination of a lack of training, lack of good health, lack of a collaborator and ultimately a lack of time before her death in 1852 at the early age of 36.

It is possible that with more time and better health, she would have published more work. But she didn’t.

1. 2

This is amazing. Looks like a very ergonomic smart contract language.

1. 1

I would like to work on a small OS for smart phones someday. Particularly targeting the new RISC-V processors.

1. 4

I suggest you take a look at Inferno: https://en.wikipedia.org/wiki/Inferno_(operating_system)

It’s already got Raspberry Pi and Android ports in progress. A smartphone version has been demonstrated. It’s the last product of the Unix family, with about 30y more development and thought than Unix itself.

1. 2

Thanks for this

1. 3

I am currently porting my algotrading program from Python to Nim for three reasons.

• It’s faster that Python
• It’s compiles into a crossplatform, single executable binary — deployment is basically uploading a single tiny executable file. No “virtualenv” , containers or other uncessantly complications
• Nim still has the ergonomics of Python (which was why I used it in the first place. So I don’t feel like I am missing out on anything
1. 1

I use Google Keep to update notes across devices.

For more short form content, telegram or a Gmail Draft

1. 6

The natural numbers also form a monoid under multiplication as well:

1 x 1 = 2

What?

1. 1

Just a typo.

1. 1

just off by 45 degrees ;)

1. 10

Corrected (I shall be remembered as the person who wrote a math textbook and made a mistake in calculating 1 * 1)

1. 2

Eh, one of the old answer guides to Spivak’s Calculus has 2 - (-2) = 0 in it, so they literally got 2+2 wrong.

1. 1

Relax, everyone makes mistakes

1. 23

Very impressive. Does it put images literally everywhere except the one place I want them to go?

1. 7

Admittedly, I never understood this behaviour until I wrote a thesis in LaTeX. Then the figure-floating-behaviour makes total sense.

1. 2

Could you please elaborate more on this?

1. 7

The float behaviour builds on LaTeX’ goal to have a harmonic typesetting result. Not to go to deep, you can give one or more of the “intents” “h” (here), “t” (top of page), “b” (bottom of page), “p” (full page) to a figure, which gives LaTeX the freedom to place the figure at the given positions. Using the intent “H” or even “H!” makes sense in some cases, but really is a misuse of the floating environment.

The idea is that you often end up with multiple figures in one place. LaTeX really watches out that figures don’t float too far away and even considers things when you have a multipage-document, such that e.g. your text is on page N and your two figures are on page N+1. It looks horrible in the editor, but if you look at the final printed out version you realize the motivation. But even if you don’t print it: Using this heuristic prevents too many figures from being in one place. What if you add more content at the front and it shifts half a page? Manually adjusting floats is almost impossible. With floats you just don’t have to worry about that.

I always use [htbp] for my figures for that reason.

1. 2

I always use [htbp] for my figures for that reason.

Oh god thesis writing flashbacks…

2. 2

Not GP but having also written a thesis in LaTeX, it’s pretty sensible. You place your \begin{figure} where it’s relevant and the image will end up positioned probably at the top or bottom of the page where you put that directive. If you have a lot of figures it will set aside entire pages for figures. Alternatively you can override it with various placement specifiers (including “put it right here”).

This avoids the two main problems you get with word processors like MS Word or LibreOffice Writer:

1. If you attach your image to text position you can get strange outcomes like a page with a one line of text, a figure, then the rest of the text below it
2. If you attach your image to page position it can end up several pages away from where it’s actually referenced
2. 3
<img src="cat.jpg"/>[!H]

1. 1

Does it put images literally everywhere except the one place I want them to go?

What do you mean? LaTeX puts images exactly where you put them, always. An image is just like a big character and it strictly follows the flow of your text. Unless you explicitly request a floating environment, LaTeX will never put an image anywhere else as it appears in your source document.

1. 1

I use hugo and a theme I developed called The Horus theme my blog lives on GitHub pages at Synchronising Life & Dreams

1. 13

The short story upon which Arrival was based, Story of Your Life by Ted Chiang, is really excellent and I’d recommend reading it if possible.

1. 3

Thanks for the recommendation.

1. 9

The author’s point’s while valid, they assume that VPNs are only used by people to remain Anonymous.

VPNs are heavily used for censorship circumvention in situation where people don’t care much about anonymity, but want to restrictions put on them by their ISP

1. 11

Turns out having a monopoly is super problematic; who knew?

1. 15

This is unrelated to being a “monopoly” (not that GitHub is one, IMHO); every US-based company – and probably EU as well – will have to deal with these kind of restrictions. As people point out in that issue, the same problems exist with GitLab. You will encounter the same issue with SourceHut as well, as Drew confirmed.

Perhaps you’ll remember similar problems when there were US crypto export restrictions back in the 90s, which was similar.

In other words, the problem is a political one. Complaints about an alleged “GitHub monopoly” – whatever merit they may or may not have – are entirely misplaced and deeply uninformed. It looks like you just read the title, and knee-jerked to “GitHub bad!” Well, okay, but this isn’t reddit and I would expect a higher standard here

1. 19

It’s a monopoly problem because if you are blocked from GitHub, you are essentially blocked from working in the entire software industry. Git was designed to be a distributed system that should be resilient to authoritarian censorship like this, but we as an industry managed to snatch defeat from the jaws of victory. A decentralized network of git servers wouldn’t have this problem.

You will encounter the same issue with SourceHut as well, as Drew confirmed.

If you have this problem with SourceHut, you spin up your own instance or pay someone in another jurisdiction to run one for you; no problem. But realistically it’s very unlikely that these laws would be enforced in a healthy ecosystem anyway even for servers hosted within US jurisdiction.

1. 5

It’s a monopoly problem because if you are blocked from GitHub, you are essentially blocked from working in the entire software industry.

Apart for that being a massive exaggeration, it’s also doesn’t make Github a monopoly.

1. 7

if you are blocked from GitHub, you are essentially blocked from working in the entire software industry.

This is massive hyperbole.

1. 8

I mean… it’s the intent of the sanctions, isn’t it? That’s the reason to put sanctions in place, to block economic cooperation. A Crimean resident working for a US-based company is economic cooperation. A Crimean resident working for a non-US-based company which relies on infrastructure provided by a US-based company is economic cooperation. If there are alternatives to the existing arrangements but companies have to spend time and money switching to them, that’s an intended effect. If the cost of switching causes some companies to fire people rather than switch, that’s an intended effect.

Generally, economic sanctions are imposed thoughtfully and narrowly, because their effects are so great and because the people most affected by them are almost always private citizens with no power to change the situation the sanctions are intended to protest. There have been many books and PhD theses written on the ethics of this. When the decision to impose sanctions is taken, broadly speaking, the more arduous it is for people to comply, the more likely it is the sanctions will achieve their policy objective.

You can certainly argue that there are alternatives to GitHub, and that in that sense the statement is exaggerated, but the political objective of the sanctions is precisely to block people from working in the software industry, to the extent that the US “owns” the software industry - and I can assure you that many policymakers do feel that sense of ownership. I do not think it’s hyperbole.

1. 5

“This is massive hyperbole” “I mean… it’s the intent of the sanctions, isn’t it?”

There’s all kinds of software engineering positions which don’t require you to be on Github. Massive hyperbole indeed. Now, you might be locked out of Silicon Valley or any other area that puts too much weight into Github activity along with other buzzword tech. Not coding projects you show them but Github specifically. I’m not even sure S.V. requires that in general.

Certainly useful if one wants to pull tech in from Github projects. There’s bypasses to do that, though.

1. 3

Thanks for this thoughtful expansion. I agree that sanctions can hit some parts of the targeted population harder than others. They are weapons after all. They’re also predicated by the notion that economic hardship can lead to a change of attitude for the targeted regime, which is problematic to say the least when regimes are authoritarian and control public opinion.

However, I was not discussing sanctions in general, nor even the specific sanctions against the Russian Federation in regards to its annexation of Crimea from Ukraine.

I was reacting to the perceived notion that software development is impossible without access to GitHub. Git was developed in 2005, GitHub launched in 2008, and presumably took a few years to reach its current dominant position. Yet people managed to develop software just fine before they existed.

1. 2

That is certainly a fair position.

2. 3

Its not hyperbole for people that use Golang.

How are they supposed to install dependencies using go get while most of the packages are stored on GitHub?

1. 4

That does seem to be an issue, yes. But Go and its ecosystem is not “the entire software industry”.

3. 6

You can still do all of that. No one – certainly not GitHub – is stopping you from self-hosting your git service using one of many publicly available tools, and many do exactly this. You’re certainly not “blocked from working in the entire software industry”, although you might run in to trouble if you’re working for a company that uses GitHub. But then again, that’ll most likely be a Western company, and they probably wouldn’t be able to hire you in the first place, so the point is rather moot.

authoritarian censorship

This is neither censorship nor authoritarian. It’s a sanction imposed due to the highly dubious annexation of Crimea by Russia. Whether it’s a good measure is debatable, but it’s not “authoritarian censorship”.

1. 3

You can still do all of that.

I can do that, but unless it’s being done by organizations who can employ Crimean residents, it does no good for them.

This is neither censorship nor authoritarian

You’re right that it’s not censorship, but I would say that forcing US citizens to punish the residents of a particular region for the crime of having their home invaded is authoritarian.

1. 6

All people are victims of circumstances, and it’s sad that some people have to suffer for decisions of other people. That said, staying in Crimea is career limiting, and it wasn’t the US who got that ball rolling.

2. 2

But realistically it’s very unlikely that these laws would be enforced in a healthy ecosystem anyway even for servers hosted within US jurisdiction.

I guess it would be impractical to enforce laws against whatever server @technomancy or @notriddle spins up, but that’s mostly a matter of the gov’t never noticing that we exist enough to check in. But for commercially hosted servers (which is always going to dominate the mainstream, because most people don’t want to mess with running a server themselves), it seems perfectly feasible for the US government to enforce trade sanctions against any realistic number of companies. Arguing otherwise would require you to either argue that the government doesn’t have enough resources to enforce trade laws in any of the many industries that are subject to regulation, or arguing that there don’t exist “healthy ecosystems” in any industry (both of those positions actually have merit, but they’re huge, general, political problems that aren’t going to be solved with improved tech).

1. 3

arguing that there don’t exist “healthy ecosystems” in any industry

I think the closest thing to a healthy ecosystem we have to compare against is the Fediverse.

It is in fact a great example of using a distributed ecosystem to work around problems with authoritarian crackdowns; in this case against sex workers in the wake of FOSTA: https://www.usatoday.com/story/news/world/2018/06/29/fosta-sex-workers-leave-twitter-switter-after-us-law/744989002/

1. 8

I think the closest thing to a healthy ecosystem we have to compare against is the Fediverse.

That’s not an industry. I mean, the sex work is commercial, but Switter itself is not. Switter does not have employees, does not pay taxes, does not sign SLAs, and if a lawsuit was brought against them, they’d either fold or have to beg on Kickstarter for help. That’s just someone, who doesn’t count as “most people”, being willing to take on the complex nastiness of running a server. Stuff like Switter can never be mainstream, because individual hobbyists can’t run the world’s mainstream social network. There simply aren’t enough of us. (which is not actually meant as a knock on Switter specifically; sex work was on the fringes of society long before they decided to host a Mastodon instance, and I’m sure it’ll work fine; the point is that it can’t replace GitHub)

More importantly, I think the Fediverse as it exists is fundamentally unsustainable, because the spam problems (you’ll notice that Switter currently has registrations closed because of spam) are only going to get worse the more popular it gets. What happened to SMTP is just going to happen to ActivityPub.

1. 2

We’re not going to make the same mistakes as SMTP

1. 7

You already did make the same mistakes as SMTP:

• ActivityPub routes based on domain name, depriving users of the ability to transparently migrate from one instance to another. The best you can do is forward between two addresses, and that still means that if the node goes away, then so does your old identity. This incentivizes people to seek out instances that they expect to be around in ten years, since once you pick an instance, you’re committed. Contrast this with the humble phone number: if my current provider announces that they’re going to close up shop, I can port by existing number to a new provider, and even when they go out of business it continues to work.

• ActivityPub allows anyone with an IP address to inject content into public view (through follow-bots). You can layer on requirements, just like email does, but anyone who’s able to meet those requirements basically has a license to spam until you get around to blacklisting them. This is fundamentally true for all public-access push-based systems, including not only email, but blog comments, the phone network, and NNTP. It is importantly absent in systems with pull-based or immutable semantics like RSS, Freenet, and BitTorrent, and in closed systems like Lobsters and RetroShare.

• ActivityPub doesn’t really nail down what you can and can’t include in a message. Different clients will have different policies when they sanitize HTML, which can result in messages getting garbled.

1. 2

We are fixing much of this in LitePub.

1. 1

I hope they improved the hardware drivers support, I had a hard time getting my GPUs to work on WSL

1. 5

Hi Guys,

I was not trying to spam in any way, nor am I in any way affiliated with the author or his company. I submitted this article because I thought it was interesting, more specifically the method in which he extracted the passwords in plain text.

I should have been more careful.

1. 7

Hey don’t worry about it, I also thought the script and the format of data storage for the passwords was interesting. I also think that the holes in the article that other people are pointing out are interesting. You’ve started a fun discussion!

1. 1

During my first semester at university, I submitted nearly all my homework using groff, and when the math part came up, I had to learn some eqn. It war really horrible, if the formula got slightly complicated, let alone when trying to write a mathematical proof.

And then there’s the general problem that troff/groff has so little good documentation, which is kind of ironic.

The good thing is that you don’t even need to know any of this to use groff, nowadays, which still produces smaller pdfs in less time. Since pandoc 2.0 has been released, a pdfroff exporter has been added that can parse TeX math and convert it to eqn syntax. Emacs calc mode can do a similar trick, but it more cumbersome.

1. 7

I’m a big fan of the eqn syntax: concise, powerful, easy to write, easy to read. TeX was heavily inspired by it, but has too many backslashes.

eqn:

x = {- b +- sqrt {b sup 2 - 4 a c}} over {2 a}


TeX:

x = {-b \pm \sqrt{b^2-4ac}} \over 2a


Plain UTF‐8:

𝑥 = (−𝑏 ± √(𝑏² − 4𝑎𝑐))⁄2𝑎


MathML:

<mrow>
<mi>x</mi>
<mo>=</mo>
<mfrac>
<mrow>
<mo>−</mo>
<mi>b</mi>
<mo>±</mo>
<msqrt>
<mrow>
<msup>
<mi>b</mi>
<mi>2</mi>
</msup>
<mo>−</mo>
<mi>4ac</mi>
</mrow>
</msqrt>
</mrow>
<mi>2a</mi>
</mfrac>
</mrow>

1. 1

The square root formula is too simple, it’s not what I’d consider “complicated”. What I was thinking about was aligned equations, using other fonts or with symbols not included in the default.

Take for example

\[fa] n >= 0: \fCcn(n)\fP ~\[==]~ C sub n = { ( 2 n ) ! } over { ( n + 1 ) ! cdot n ! }


or

.EQ L
wp(\fC\(dq df := df * x; x := x - 2\(dq\fI, I)
.EN
.EQ I
\(== ~ wp(\fC\(dq df := df * x; x := x - 2\(dq\fI, df cdot x !! = n !! ~ \(AN ~ x >= 0)
.EN
.EQ I
\(== ~ wp(\fC\(dq df := df * x\(dq\fI, df cdot ( x - 2 ) !! = n !! ~ \(AN ~ x - 2 >= 0)
.EN
.EQ I
\(== ~ wp(\fC\(dq\(dq\fI, df cdot x cdot ( x - 2 ) !! = n !! ~ \(AN ~ x - 2 >= 0)
.EN
.EQ I
\(== ~ df cdot x cdot ( x - 2 ) !! = n !! ~ \(AN ~ x >= 2
.EN


both which I remember took a white to correctly typeset.

2. 2

Eqn IMO has a cleaner syntax compared to main stream alternatives like MathML & MathJax.

I am still not sure why it didn’t become popular

1. 4

I attribute it to Joe Ossanna’s untimely death and troff being proprietary to AT&T.

1. 3

Nice overview. I recommend adding Runtime Verification Inc’s work under verification given what they’re doing will be more accessible than Coq. For instance, their RV-Match tool is push-button with low, false positives. I’m not sure if they have one like that for Ethereum contracts. If not, they’re probably working on it now. They have a list of successful work on their page and blog.

Also, their K Framework is open source for folks to build on.

1. 3

Runtime Verification Inc has done fantastic work.

I am happy that they worked on semantics for smart contract languages like Vyper & Solidity.

1. 3

Wait, I forgot that @lojikil works at a company that built Manticore and Slither. Manticore does symbolic execution on smart contracts. Slither does static analysis on Solidity code. Both are AGPLv3 with commercial licenses available. Since I don’t do smart contracts, I can’t tell you any more than that. :)

Trivia: Slither’s name was chosen after they held a focus group asking project managers and finance experts to visualize things that helped them sleep at night. That’s because the product was supposed to help them sleep at night. They arrived at Slither. Some outsiders were baffled at the result.

Trivia: The above trivia may or may not be a work of fiction. Its author is skeptical about the user considerations that went into choosing the name, though. ;)

1. 2

tl;dr: there’s lots of formal verification going on in the space, and lots of collaboration too, and regardless of what anyone thinks of cryptocurrency and smart contracts, it’s super interesting to see the space evolve

The RunVer folks do some great work with K; K for EVM, for eWASM, for client projects, it’s pretty interesting. The ChainSecurity folks also have SOLTIX and VerFx (I think, the name eludes me, I still haven’t processed coffee) for testing Solidity compilers and smart contracts respectively. Likewise, the Consensys Diligence folks have Mythril Classic, their new MythX platform, and a few other things.

On our side, we have a suite of tools we’ve released. Beyond what Nick mentioned, these include:

Also, Slither contains an IR called “SlithIR”, which we use internally for additional tooling. There’s also work on symbolic computation & abstract interpretation atop SlithIR.

Regardless of what you think of the space, the thing I find most fascinating is that there are several companies working in the formal verification space and helping clients really understand the correctness of the code they’ve written. This means understanding the semantics of terrible languages like Solidity (and better ones like Vyper, hi Bryant!), the EVM, contributing to discussions like “should we add static jumps to EVM” or “Is you gas calculation horribly broken?”. You’ll note the EIP-1283 link is a collaboration between ToB, ChainSecurity, and the Eveem teams; many companies just show up and collaborate to make things better.

1. 3

“regardless of what anyone thinks of cryptocurrency and smart contracts, it’s super interesting to see the space evolve”

Heck yeah, it is. I call out cryptocurrency and blockchains as mostly useless. Yet, the cryptocurrency verification scene is awesome. Between it and CompSci’s latest, we’re in a golden age of applied, formal verification being able to have an impact in the world. My recommendation was people learn verification, start in these companies (or start companies), and build on existing tools with lots of academic collaboration to make them cover more use cases. Aka, leverage the piles of money to build what they want along with what we all need. Although most focus on proof, I like that you have a mix of tools including testing and verification, HLL’s and binary. That’s consistent with high-assurance security using a mix of tools to cover any’s weaknesses. Smart.

That leads to only gripe I have in this space. Aside from RVI w/ K, what few I’ve seen aren’t building on the tools that already have strong ecosystems. That includes Why3 (esp Why3), Simpl w/ HOL used in seL4 (eliminates compiler), whatever CakeML people are using, ACL2, KLEE, and so on. As each extension happens, we would get new theories or plugins that cover certain kinds of properties that others can reuse. Why3 (software) and ACL2 (hardware) crowds were doing this the most with lots of automation (good for accessibility). That’s what I want to see more of. Then, maybe spec/property-based, test generation supported for each thing they contribute to empirically test the proven code. Eventually, we have toolchains that can handle about anything really critical.

The crypto-verification communities are doing lots of good work. They have even more potential than that, though. The kind of potential that kicks off future projects in unrelated areas. That’s what I want to see next.

1. 3

Yes, but what for? Some of us don’t have things to blog.

1. 7

do you have any thoughts whatsoever? You probably have things to blog about. Write a poem, a tidbit, a story, whatever comes to mind. I have no idea what I blog about. My fingers produce digital vomit on the screen. It’s pretty awesome!

1. 14

What most people don’t realize is that the simple comments they have on websites like Lobsters along with the stuff they published on Instagram, Facebook & Twitter probably qualify as blogposts.

A personal website is a fantastic way to curate these personal thoughts we ocasionaly have.

1. 4

Yeah a few times I’ve made a long comment on some reddit/HN thread and I realise it’ll probably be seen by about 3 people, but contains a good explanation of something. If I had a blog I could post to easily I would use it.

1. 5

It’s really easy to get started, if have a github account. Follow these directions, and you can have a blog up in 10 minutes: https://github.com/barryclark/jekyll-now

1. 1

Also if you want the ability to author and edit posts with a nice UI, forestry is really good IMO.

2. 3

Many of my blogposts are copypasta of things I wrote on HackerNews/StackOverflow/etc. (with links back to those comments). I can’t recall doing it from a lobste.rs comment yet, but that’s probably just the slower rate at which this site moves compared to those firehoses.

The two aspects which help are:

• Having a specific thing to write about (a submission, question, comment, etc.), as opposed to some nebulous idea for a blog post (analogous to staring at a blank page).
• A little back-and-forth with others, whose different opinions can bring fresh perspectives on our thoughts, and which gives a sense for the ‘audience’ that we’re writing for. This could be antagonistic (“How could something think X? I can write a whole treatise on why they’re wrong”) or cooperative (“I find X so natural that I didn’t realise people struggled with it, maybe addressing their particular difficulties would be helpful for others too”)
1. 3

Working on a Mobile Money package for Flutter ✌️