Readit NewsWe need automated ways of converting Python and other popular languages to TLA+ with ways of verifying that they were translated correctly. Otherwise it seems like too much work for most purposes.
Converting from Python to TLA+ could be considered a form of denotational semantics. It's a ton of work to model the denotational semantics of even simple computer programs. I imagine an automatic translation of a nontrivial program would be infeasible to work with, but curious if there is active research or progress in this field.
Cieplak commented on Linear transformers are faster after all manifestai.com/blogposts/... · Posted by u/JoelEinbinder
What did they use to build this site? I could have sworn I saw what looked like LaTex when it was loading?
Looks like quarto. The LaTex you saw may have been MathJax.
$ curl -s https://manifestai.com/blogposts/faster-after-all/ | grep generator
<meta name="generator" content="quarto-1.3.450">There's a command-line utility called pixd [1] that generates similar data visualizations on the command line. That said, it only shows static representations of binary data and is not nearly as cool as buredoranna's animated gifs showing filesystem changes over time.
It can be helpful to plot these sorts of pixel arrangements on a Hilbert curve, rather than plotting pixels line by line. I learned this trick from a Ghidra plugin called cantordust [2]. 3blue1brown offers some mathematical intuition for the effectiveness of a Hilbert curve pixel arrangement [3].
[1] https://github.com/FireyFly/pixd
[2] https://inside.battelle.org/blog-details/battelle-publishes-...
Thanks Neil Sloane and OEIS.