muraiki

When you write a recursive function, Lean’s kernel requires a termination proof, unless the function is a partial or marked as unsafe. In those cases, they can’t be used in proofs. https://lean-lang.org/doc/reference/latest/Definitions/Recur...

Oh whoops, thank you for the correction! I didn't realize that.

The article says that AWS's Cedar authorization policy engine is written in Lean, but it's actually written in Dafny. Writing Dafny is a lot closer to writing "normal" code rather than the proofs you see in Lean. As a non-mathematician I gave up pretty early in the Lean tutorial, while in a recent prototype I learned enough Dafny to be semi-confident in reviewing Claude's Dafny code in about half a day.

The Dafny code formed a security kernel at the core of a service, enforcing invariants like that an audit log must always be written to prior to a mutating operation being performed. Of course I still had bugs, usually from specification problems (poor spec / design) or Claude not taking the proof far enough (proving only for one of a number of related types, which could also have been a specification problem on my part).

In the end I realized I'm writing a bunch of I/O bound glue code and plain 'ol test driven development was fine enough for my threat model. I can review Python code more quickly and accurately than Dafny (or the Go code it eventually had to link to), so I'm back to optimizing for humans again...

Try out Forker shorthand. You can learn it gradually, and the first steps are omitting vowels and simplifying some letters. You then progress to various abbreviations. Ultimately, it's based on the English cursive so there's nothing too exotic to learn in terms of orthography, although I guess if you are younger there is a chance you never learned a cursive style! I'm a novice but feel like it doesn't hurt readability that much, and it's quick to learn.

Quick intro: https://imgur.com/a/zYyON

> Research has long shown that layoffs have a detrimental effect on individuals and on corporate performance. The short-term cost savings provided by a layoff are often overshadowed by bad publicity, loss of knowledge, weakened engagement, higher voluntary turnover, and lower innovation — all of which hurt profits in the long run. To make intelligent and humane staffing decisions in the current economic turmoil, leaders must understand what’s different about today’s larger social landscape. The authors also share strategies for a smarter approach to workforce change.

https://hbr.org/2022/12/what-companies-still-get-wrong-about...

One option for C++14 is the Au units library. Here's a comparison to other unit libraries, including mp-units: https://aurora-opensource.github.io/au/main/alternatives/

“Graph” here means the directed acyclic graph encoding the causal relationships, not a chart of a distribution.

There are other benefits to Bayesian data analysis besides being able to handle limited data. There are problems with the outputs of frequentist analysis around the quantification of uncertainty. For instance, from simulation studies we know that the aleatoric coverage probability for confidence intervals of a selected confidence level varies depending on the size of the difference in plausibility between the null and alternative hypotheses. And a given confidence interval says nothing about epistemic uncertainty for this particular experiment. This can make the outputs of frequentist analysis difficult for stakeholders to utilize, whereas Bayesian epistemic probabilities are generally more easily understand by stakeholders, and can directly feed quantitative decision analysis methods.

A good introduction to some additional problems with frequentist methods vs Bayesian and likelihoodist methods is this: https://gandenberger.org/2014/08/26/intro-to-statistical-met...

An interesting book on adapting frequentist methods to create confidence distributions that can better express uncertainty and can optionally incorporate prior information using likelihood functions is this: https://www.cambridge.org/core/books/confidence-likelihood-p...

I remember that there was a company that would somehow print out the 3DS photos in a way that they could be seen in 3D (probably with limited viewing angles). I'm sure there's some photography term here that I'm totally unaware of. I'd love to find a way to do this.

Here's an article from the SEI covering the problems with using Ghidra for malware analysis of Rust code. See "Binary Analysis Without Source Code" https://insights.sei.cmu.edu/blog/rust-vulnerability-analysi...

Ok, here's a better article from CMU's SEI. See "Binary Analysis Without Source Code".

> In general, the layout used by the Rust compiler depends on other factors in memory, so even having two different structs with the exact same size fields does not guarantee that the two will use the same memory layout in the final executable. This could cause difficulty for automated tools that make assumptions about layout and sizes in memory based on the constraints imposed by C. To work around these differences and allow interoperability with C via a foreign function interface, Rust does allow a compiler macro, #[repr(C)] to be placed before a struct to tell the compiler to use the typical C layout. While this is useful, it means that any given program might mix and match representations for memory layout, causing further analysis difficulty. Rust also supports a few other types of layouts including a packed representation that ignores alignment.

> We can see some effects of the above discussion in simple binary-code analysis tools, including the Ghidra software reverse engineering tool suite... Loading the resulting executable into Ghidra 10.2 results in Ghidra incorrectly identifying it as gcc-produced code (instead of rustc, which is based on LLVM). Running Ghidra’s standard analysis and decompilation routine takes an uncharacteristically long time for such a small program, and reports errors in p-code analysis, indicating some error in representing the program in Ghidra’s intermediate representation. The built-in C decompiler then incorrectly attempts to decompile the p-code to a function with about a dozen local variables and proceeds to execute a wide range of pointer arithmetic and bit-level operations, all for this function which returns a reference to a string. Strings themselves are often easy to locate in a C-compiled program; Ghidra includes a string search feature, and even POSIX utilities, such as strings, can dump a list of strings from executables. However, in this case, both Ghidra and strings dump both of the "Hello, World" strings in this program as one long run-on string that runs into error message text.

https://insights.sei.cmu.edu/blog/rust-vulnerability-analysi...

My favorite decaf: https://www.defer.coffee/coffee-tea/p/palmera-decaf

Another good one: https://www.convivecoffee.com/shop/decaffeinated-colombia

The use of Rust has particular implications for malware analysis: https://c3rb3ru5d3d53c.github.io/2022/08/malware-reversing-r...

So yes, it's relevant.

With the mention of memristors, this sounds kind of similar to what Wolfram recently said about hardware for neural networks that can simultaneously be memory and compute:

> But even within the framework of existing neural nets there’s currently a crucial limitation: neural net training as it’s now done is fundamentally sequential, with the effects of each batch of examples being propagated back to update the weights. And indeed with current computer hardware—even taking into account GPUs—most of a neural net is “idle” most of the time during training, with just one part at a time being updated. And in a sense this is because our current computers tend to have memory that is separate from their CPUs (or GPUs). But in brains it’s presumably different—with every “memory element” (i.e. neuron) also being a potentially active computational element. And if we could set up our future computer hardware this way it might become possible to do training much more efficiently.

https://writings.stephenwolfram.com/2023/02/what-is-chatgpt-...

Flagged because this "secret" has been known since 2020 (the article has been updated to state this but kept the clickbait title)

It's worth noting that the paper was submitted in August of 2021. So perhaps it took a year to develop the methodology and get the paper ready for publishing. They did use separate training, validation, and test sets for data, although we do need to trust that the test set was only used a single time. To whatever extent the model doesn't do as well in 2022 as it did at the time it was created, that comes down to concept drift and data drift.

"The training, validation and test data sets are generated without overlap from periods in sequence. Successive periods of 400, 12, 40, 40 and 12 h are used to sample, respectively, training, validation, and test data, with the two 12 h periods inserted as hiatus."

Looks like two studies contradict that: https://www.psychologytoday.com/us/blog/open-gently/201802/a...

Ha, I did the same thing, and in Perl nonetheless! My poor boss. I guess he forgave me since we’re still friends!

Edit: A good book: https://en.m.wikipedia.org/wiki/Higher-Order_Perl

One thing that helped me with this was getting good quality pencils where I can use a minimal amount of pressure (a non-ballpoint pen also works). I also had to unlearn gripping the pencil hard and tensing my wrist. Good handwriting doesn't require tension: tension can occur because of misplaced effort at trying to write more nicely.

I relearned the motions of how to handwrite using Briem's handwriting repair curriculum: https://sites.google.com/view/briem/free-books/handwriting-r... Now I really enjoy writing by hand. Of course if I'm writing quickly the quality isn't as nice as when I can take more time.

There is a section on the site specifically about hand tension here: https://sites.google.com/view/briem/handwriting/writing-cram...

> Books on modeling often jump right into math and methods. Drowned in detail, it can take years to appreciate the assumptions and limitations of the various modeling mindsets.

> Written in a clear and concise style, Modeling Mindsets introduces approaches such as Bayesian inference, supervised learning, causal inference, and more.

> After reading this book, you will have a much better understanding of the different approaches to modeling and be able to choose the right one for your problem.

https://book.modeling-mindsets.com/

Edit: Ah darn, I forgot about this part: "You should feel comfortable with at least one of the mindsets in this book". So perhaps not the best start if you don't have a base in at least one method. For frequentist statistics, consider https://www.openintro.org/book/os/

Woods and Wyrms

Gives a bit of a boost to the ranger class.

lol, they actually put it as a zinger at the end of the announcement:

> Thanks, as always, for being a part of this journey.

I have to say, the tone and execution of this announcement has killed all interest I had in dbt. I don't want to have to explain company behavior like this to my boss when proposing the use of a new tool.

Or it could be that she is experienced with both software and law, and that her assessment is different than yours.

> Kate’s passion for open source began in law school, under the tutelage of Eben Moglen, long-time attorney for the Free Software Foundation, founder of the Software Freedom Law Center, and author of the GPL 3. She interned at the Electronic Frontier Foundation and helped write the first complaint against the NSA for warrantless wiretapping.

> At VMware and ServiceNow, she dedicated her time to designing, building, and testing internal compliance tools in collaboration with their respective internal tools teams. She is no stranger to writing specs, creating wireframes, and massive amounts of QA. So much so, that Kate and her husband, Steve Downing, co-founded Critterdom LLC, a software company whose Open Sorcerer product substantially cuts down the time it takes to manually review source code for licenses and create a customer-facing disclosure of that source code.

https://katedowninglaw.com/about/

Formula E has “attack mode” sections that temporarily boost the electric car’s power by 30kW: https://www.fiaformulae.com/en/championship/attack-mode

Venmo has continually failed at privacy: https://www.legalreader.com/venmos-at-it-again-privacy-issue...

Privacy is an area where Apple tries to differentiate. It’s not great that this is Apple only, but it’s also nice that it just works.

Only the slides are available, but the presentation "AI is Not Magic: Machine Learning for Network Security" at CMU's FloCon in 2020 was about this: https://resources.sei.cmu.edu/library/asset-view.cfm?assetid...

Flagged because it looks like this site has been XSS'd

Apology from the PI, permanent suspension of sending emails, possible follow up emails telling people to disregard the original emails, and commitment to a formal research ethics study: https://twitter.com/jonathanmayer/status/1472427321047101442