The Lean Programming Language

The Lean Programming language is being used to create a new proof of Fermat's Last Theorem. Some lecture notes from London's Imperial College set the scene.

Theoretical Foundation (DTT)

Dependent type theory (DTT) is the theoretical foundation of Lean (the link provided takes you into the Lean manual and gives a brief intro to the theory) which bears "categorical semantics".

Getting Started with Lean

• The best way to get started in Lean is to read Functional Programming in Lean.
• The next step is to read Theorem Proving in Lean.

Who created Lean

Lean was created by Brazilian computer scientist Leonardo de Moura, in 2013, when he worked in Microsoft Research (where he worked for 16 years). 

Leonardo is now Senior Principal Applied Scientist at AWS, where he works in the Automated Reasoning Group.  This group does a lot of work in Provable Security and Software Assurance.

Lean is available under the Apache 2.0 license.

Parity between Azure and AWS

It is worthwhile to maintain knowledge parity between Azure and AWS. 

If you use a cool thing in Azure, chances are the same functionality exists in AWS (e.g. managed kubernetes service - known as AKS or EKS in respective clouds) and so you should know how to do same cool thing in AWS.

Cloud economics may dictate future decisions.

A Nod to AWS EKS

AWS EKS (Elastic Kubernetes Service) is a fully managed Kubernetes service provided by AWS. 

EKS simplifies deployment and management of containerized applications using Kubernetes. Users need not manage the Kubernetes control plane or nodes manually.

Jargon warning: 

The Kubernetes control plane is the central management utility of a Kubernetes cluster. 

It maintains cluster state, making decisions about the cluster and responding to cluster events. It is made up of several key components that work together.

AWS basically runs the control plane for you.

There are a number of use cases suggested by AWS.

LiteLLM - Gateway to 100+ LLMs

LiteLLM is an open source library that lets you call into over 100 LLMs.

One aspect of calling into lots of LLMs is you have lots of API keys. These are stored in environment variables like OPENAI_API_KEY, ANTHROPIC_API_KEY - you can also feed these as direct arguments in code to LiteLLM.

You can also integrate a secrets manager like AWS Secrets Manager, Azure Key Vault and Google Secret Manager.

Amazon Bedrock

Amazon Bedrock is the AWS fully managed platform for building generative AI services. It is basically (like LangChain) a unified API to call into various models and provides managed capabilities like retrieval-augmented generation (RAG), vector embeddings, guardrails and agents/agent orchestration.

The AI Agent Prevention Society

One of the obstacles to AI agents becoming all powerful is the technology infrastructure that actively seeks to obstruct agents.

This technology has various names, one being WAF, or web application firewall.  

The purpose of a WAF is to stop web applications from common attacks. 

Recall the OWASP Top Ten Risks? Some of the motivation behind these protections are good - for example, guarding against bot-driven DDoS attacks.

There are various vendors and products in this space; such as Imperva WAF, Cloudflare, Akamai Site Defender, AWS WAF, Azure Web Application Firewall and Google Cloud Armor.

These solutions are all effective at detecting and blocking agents, headless browsers, scrapers, credential stuffing bots (where leaked usernames and passwords are used across numerous websites to exploit potential duplication) and automated (even if legitimate) login attempts.

Action taken could range from limiting requests based on IP, presenting CAPTCHA challenges and blocking certain geographies.  However, these actions may prevent legitimate bots from using required services, or performing agentic actions on behalf of legitimate users.

Ingress and Egress Fees

Ingress and egress fees refer to the cost of data transfer into and out of the cloud.

• Ingress fees are typically zero - allowing users to upload data to Amazon S3 or Azure Blob Storage with no additional charge. 
• Egress fees are typically charged when data exits the cloud. These fees can differ significantly between providers and source and destination region.

Hosting on S3 will set you back $0 for 1 GB download per month, and around 1000 downloads of a 50MB file will cost you just under $5 a month.

Leaning in on Lean

Lean is an open-source programming language and proof assistant. AWS uses Lean and "verification-guided development" to verify Cedar, the AWS authorization policy language.

Lean is being used to attempt a computer proof of Fermat's Last Theorem using the blueprint (note: the blueprint link no longer works).

AWS S3 (and Auth Methods) for Azure Folks

Amazon S3 is something akin to Azure Blob Storage. 

A quick revision of Azure Blob Storage: 

Azure Blob Storage is a general-purpose cloud storage option for cloud native workloads.  

It supports WORM operating scenarios (Write Once Read Many) aka WORM-compliant storage (which prevents data from being edited or deleted). Role based access control (RBAC) is supported as is authentication with Microsoft Entra (formerly Azure Active Directory).

Amazon S3 (Simple Storage Service) is a similar offering in AWS.

The services are exposed as a web service with a custom HTTP scheme known as keyed-HMAC (Hash Message Authentication Code).  A more "high level" authentication option is available via AWS IAM.

LLM Training Data

LLMs are trained on large data sets.  One such data set is Common Crawl which consists of 250 billion Internet pages with 3-5 billion pages added each month.  This is petabytes worth of data (1 petabyte = 10^15 bytes of digital information). The data is stored on Amazon's S3 service allowing direct download or access for Map-Reduce processing in EC2.

Is Blazegraph now Amazon Neptune?

Blazegraph is an open source graph database written in Java. It has been abandoned since 2020 and is used in production by the Wikidata Query Service. It is licensed under GPL version 2.0. 

 

Amazon Neptune is Amazon's high performance graph database available through AWS. As Amazon acquired Blazegraph developers, it is possible Neptune is the new, maintained incarnation of Blazegraph.

Progressive Rollout (aka "Canary Deployment") in the Cloud

A canary deployment is an old concept with a new branding in the age of cloud, and terminology-wise is used by both Google, AWS and Azure. Kubernetes technology is one way to manage canary deployments.

Canary deployments are progressive rollouts where new functionality is released to a subset of specially selected users. Therefore the canary deployment runs in parallel to current production deployment used by your regular users. This gives you more time and space to test the reliably of new features "in the wild".

So-called "Safe" Kernel Programming with eBPF

eBPF technology has roots in the Linux kernel. It is software designed to run programs in a privileged context within an operating system kernel in a sandboxed environment.  This is done without touching kernel source code or loading kernel modules.  A more complete description can be found on ebpf.io.

The use of the acronym eBPF is historic. BPF stood for Berkeley Packet Filter and eBPF was the extended version. eBPF now does lots more than packet filtering so the appropriateness of this meaning is defunct. The original BPF, mostly obsolete, is sometimes now called cBPF (classic BPF) to distinguish it from the eBPF concept.

A more technical guide to the technology can be found here on the Cilium website. Cilium is a tool built on eBPF used in Google Kubernetes Engine (GKE) and in EKS Anywhere on AWS (for on premise container management).

AutoScaling in the Cloud - Like Load Balancing, But Different

Autoscaling allows scalability in the cloud by allocating the "right" number of active servers for a given "load". There is also a resiliency element as loss of capacity due to application or hardware failure can be compensated by autoscaling.

Companies like Netflix use autoscaling features in AWS EC2 (Elastic Compute Cloud) - note: autoscaling was officially added to EC2 in May 2009. Netflix declared a policy of aggressive scale-up and cautious scale-down had the optimal effect. In 2013, Microsoft announced addition of autoscaling to Azure.