Use of Mathematical Induction in Proofs of Program Correctness

Robert Floyd introduced MI as a systematic method to prove the correctness of computer programs in his 1967 paper "Assigning Meanings to Programs", written at the then Carnegie Institute of Technology, supported by DARPA.

This directly inspired Tony Hoare's axiomatic semantics and the development of Hoare logic (also known as Floyd-Hoare logic).

Floyd acknowledges gestation of these ideas by Perlis and Gorm, albeit in unpublished papers.

Mathematics in VS Code with Lean

Formalizing mathematics is now possible in VS Code with Lean. See the manual here. Extension here.

Lean functionality is exposed in the UI via the universal quantifier at the top right of VS code.

Consider copying the MIL folder, containing key examples, so you can tinker with the example code.

MIL = Mathematics in Lean.

When you download the MIL, you will see a flurry of activity in your Output Console in VS Code. This will include reams of stuff relating to "Fetching Mathlib build artifact cache" and thousands of file downloads.

You will also see the incantation "lake build" which is the primary build command in the Lean build system.

Advice on how to work through the MIL textbook from the official website - "working through the exercises is central to the experience".

Note: when reading Lean files in VS code turn off Unicode character highlighting (Control-, to get into settings, and update Text Editor settings).

kdb+ - An Intro

kdb+ is a high-performance time series database and analytics engine powered by a vector language q. It has been in existence for over 30 years.

It uses columnar storage for efficient querying. For example, if you have temperature readings, taken at 5 minute intervals, you can pull out the whole vector of temperatures in a single query (you are pulling the full time series vector as opposed to a reading from a time series).

If you have corresponding humidity readings, you can do a similar query.

This avoids reading entire rows even if only one field is needed. Typical relational databases query cross-sectionally.

Open Source - and Goldman Sachs??

Goldman Sachs has open sourced some of its code.

The Lean FRO Year 3 Roadmap

Changes to Lean - as articulated by Lean FRO's Y3 roadmap.  

Some items will for sure be done, some may be pushed to Y4.

All roadmap content can be found here.

While we are there, let's say thank you to the Lean Team.

The Draw Tab in Word

The Draw tab in the Word ribbon is a great feature - but it may be turned off by default.

To turn it on do the following:

1.    File

2.   Options

3.   Customize Ribbon

4.   Select Draw

This will enable you to use a freeform marker in your Word doc.

Theorem Proving in Lean - What Makes Dependent Type Theory Dependent?

This precis is based on the Lean Manual, Section 2.8.