ubj

Good catch, link updated!

This. Lean does not remove human responsibility, but it does assist in reducing the surface that the human needs to inspect and verify.

Now, there is also debate about what is lost when humans don't understand the proof body itself. It's a fair concern, and one we'll probably be wrestling with for some years.

> and/or have infants ricocheting around your home like screaming DVD logos

Slightly off topic, but as a parent I found this hilarious and will now be closely watching to see if any of my own screaming logos ever perfectly hit the corner of a room.

I've said this before, but it's interesting to see momentum go back and forth between the flexibility and ease of everyday language, and the formal rigor of programming languages.

It feels like we are still discovering the optimal operating range on a spectrum between these two domains. Perhaps the optimal range will depend on the specific field in question.

Matlab is an great tool, if you can afford it.

It was a very unpleasant feeling when I graduated from my PhD and realized that most, if not all, of the Matlab scripts I had used for my research would now be useless to me unless I joined a company or national laboratory that paid for licenses with the specific toolboxes I had used.

I'm glad that a significant portion of tools in my current field are in open source languages such as Python and Julia. It widens access to other researchers who can then build upon it.

(And yes, I'm aware of Octave. It does not have the capabilities of Matlab in the areas that I worked in, and was not able to run all of my PhD scripts. I have not tried RunMat yet, but am looking forward to experimenting with it.)