HN Books @HNBooksMonth

I have been intrigued by the idea of visual coding tools for many years, but these kind of tools have always disappointed me. They remind me of the system used to teach small children to program in the programming language Scratch, see [Scratch].

I prefer to "visualize" my code as manipulating a set of logical assertions that characterize the state of the computation, ultimately reaching the point where the state of the computation's properties satisfy the requirements. Somewhat like that explained in [Gries1987] and [Dijkstra1976]. Visual tools are just too coarse to capture the details necessary to ensure correctness or real-life requirements.

While UML diagrams sometimes help to make sense of a complex set of OO Class relationships, this is far from how I normally work with the meaning of code in my head while programming.

[Scratch] https://en.wikipedia.org/wiki/Scratch_(programming_language)

[Gries1987] https://www.amazon.com/Science-Programming-Monographs-Comput...

[Dijkstra1976] https://www.amazon.com/Discipline-Programming-Edsger-W-Dijks...

⬐ coldtea

>I prefer to "visualize" my code as manipulating a set of logical assertions that characterize the state of the computation, ultimately reaching the point where the state of the computation's properties satisfy the requirements

OTOH, functional code should be more like a pipeline (graph), and thus better suited for visualisation.

5) advanced: https://www.amazon.com/Science-Programming-Monographs-Comput...

If you are tempted to dig further into these techniques there's this book:

https://www.amazon.com/Science-Programming-Monographs-Comput...

Heck, the basic methods of writing provably correct programs have been explained in plain English since at least the 70s:

https://www.amazon.com/Discipline-Programming-Edsger-W-Dijks...

https://www.amazon.com/Science-Programming-Monographs-Comput...

This is not some rocket science type verification with a dependently typed theorem prover language, it's fairly simple paper and pencil logic. It should not be hard to adapt it to Solidity specific concepts like running out of gas.

The reason these techniques are mostly ignored is that the techniques don't scale at all to large programs calling APIs with imprecise semantics (e.g. filesystem, network), and most people would rather publish imperfect software and iterate rather than spec everything up front. Well, unlike most software, contracts are not large, their semantics are meant to be 100% precise, and most people would rather take the time to make sure a contract does what it claims to do rather than discover a bug afterwards. I would hope.

⬐ None

None

⬐ skybrian

Calling it "imprecise semantics" is quite the understatement.

The environment software runs in is often scarcely understood at all. Operating systems and web browsers change without notice due to auto-upgrades. Libraries are often used without understanding their implementations, and they're also constantly being upgraded. Users can install plugins that introduce bugs that can't be reproduced in the test environment.

You can't build an accurate mathematical model of an environment you haven't observed. Integration tests (run against many platforms) and production logging help, but there are still plenty of unknowns.

⬐ simplify

How do you normally handle those unknowns?

⬐ skybrian

Users submit bugs and the reply is sometimes "cannot reproduce." :-)

But the more serious projects I've worked on use analytics and have semi-automated ways for users to send you stack traces and logs when they notice a bug.

Also, it's helpful to have a continuous integration setup that automatically runs integration tests on many platforms.

⬐ ori_b

Usually, by crashing or exhibiting bugs and misbehavior.

⬐ serhei

Imitating other code that is known to work [1]. Lots of testing. Fixing the bug when someone runs into it and complains (a viable last-resort for almost anything besides a Solidity contract).

[1]: For example, when working with filesystems, people write code that they saw other people using. The code may or may not work as designed depending on the specific filesystem. see e.g. https://danluu.com/file-consistency/

@jhck, drothlis: Thank you very much to both of you, those suggestions are exactly what was asked for. I'd upvote you more if I could. :)

Both the Gries book and Stepanov's book have really impressive reviews on Amazon, am looking forward to diving into them.

http://www.amazon.com/Science-Programming-Monographs-Compute...

http://www.amazon.com/Elements-Programming-Alexander-Stepano...