redo homepage

I wasn't happy with the landing page. I've redone the text and layout. Happy to have better script examples.

Author: imaginator

docs/getting-started/index.md renamed to docs/getting-started/projects.md

@@ -1,56 +1,46 @@
 ---
+title: A typed, combinator-based, functional smart contract language without loops or recursion, designed for Bitcoin-like blockchains.
 hide:
-  - navigation
   - toc
-  - title
 ---
 
-## Key Features
+<div class="grid cards" markdown>
 
-### Expressive Smart Contracts
+- ### :material-code-braces: Expressive Smart Contracts
+Simplicity lets you define precise smart contracts with more structure than Bitcoin Script while remaining statically analyzable. Encode multi-step financial flows, conditional transfers, and asset logic in a form that can be reviewed and reasoned about.
 
-Simplicity allows developers to write contracts that go beyond the limitations of Bitcoin Script. Complex financial workflows, conditional payments, and tokenized assets can all be encoded efficiently and safely.
+- ### :material-gauge: Predictable Resource Usage
+Each program has a statically bounded cost. You know the upper execution bounds before funding a transaction, avoiding unpredictable fee dynamics.
 
-### Predictable Resource Usage
+- ### :material-microscope: Formally Specified
+The semantics are formally defined and suitable for machine-checked proofs. You can prove safety properties (e.g. no unauthorized spend path) and have high assurance the implementation matches the specification.
 
-Every Simplicity contract has clearly bounded computational costs. This ensures contracts run reliably on-chain without unexpected fees or execution failures.
+- ### :material-shield-check: Enhanced Security
+No loops or unbounded recursion, deterministic evaluation, and explicit control flow eliminate broad classes of runtime failure. Behavior matches the committed program; no hidden side effects.
 
-### Formally Specified
+- ### :material-link-variant: Seamless Bitcoin and Liquid Integration
+Designed for the Bitcoin-style networks. On Liquid you can bind assets and amounts while still benefiting from confidentiality at the transaction layer.
 
-Simplicity smart contracts can be formally specified using mathematical proof assistants, enabling rigorous verification of their behavior. This ensures that contracts behave exactly as intended, significantly reducing the risk of critical bugs and security vulnerabilities.
+- ### :material-source-branch: Support for Conditional Logic
+You can encode conditional payments, options, staged settlement, and automated triggers directly on-chain without relying on off-chain escrow logic or custodians.
 
-### Enhanced Security
+- ### :material-package-variant-closed: Compact and Efficient Design
+A small combinator core and Merkle-structured programs keep on-chain footprints low. Verification costs remain predictable and amenable to static analysis.
 
-Contracts are designed to behave exactly as written, reducing the risk of bugs or unintended outcomes. Users and institutions can trust that their rules and conditions will be enforced correctly.
+- ### :material-account-group: Compatibility with Multi-Party Workflows
+Multi-party spending policies, staged cooperation, and recovery paths are expressed as explicit branches. Participants retain sole control of their keys throughout.
 
-### Seamless Bitcoin and Liquid Integration
+</div>
 
-Simplicity is built for Bitcoin-style blockchains and Liquid, making it easy to integrate with existing blockchain infrastructure. Tokenized assets, settlements, and decentralized finance workflows can leverage its native compatibility.
-
-### Support for Conditional Logic
-
-Developers can encode conditional payments, options, and automated triggers directly into contracts. This enables more sophisticated financial products without relying on external intermediaries.
-
-### Compact and Efficient Design
-
-Contracts are optimized for on-chain execution, keeping size and operational overhead minimal. This allows for faster transaction processing and reduced blockchain load.
-
-### Compatibility with Multi-Party Workflows
-
-Simplicity can handle multi-party agreements, such as escrow-free marketplaces or collaborative finance operations. Parties can interact securely without giving up control to a central authority.
-
-## Example
-
-A basic pay-to-pubkey SimplicityHL program looks like this:
-
-```rust
+``` rust title="pay to pubkey" 
 fn main(pubkey: Pubkey, funds: Funds) -> Funds {
     let (witness = _, funds) = commit(
         Witness = ValidSignature(pubkey, funds),
         funds,
     );
     funds
-}
+}// (1)!
 ```
 
-This compiles to Simplicity combinators that can be formally verified and executed on-chain.
+1.  This compiles to Simplicity ready for on-chain execution. More involved scripts can execute [reverse Dutch auctions](https://delvingbitcoin.org/t/writing-simplicity-programs-with-simplicityhl/1900).
+

docs/index.md

@@ -56,6 +56,8 @@ theme:
         icon: material/brightness-4
         name: Switch to system preference
 markdown_extensions:
+  - attr_list:
+  - md_in_html:
   - attr_list:
   - pymdownx.emoji:
       emoji_index: !!python/name:material.extensions.emoji.twemoji
@@ -123,7 +125,8 @@ edit_uri: edit/main/docs/
 
 nav:
   - Getting started:
-      - getting-started/index.md
+      - index.md
+      - Projects: getting-started/projects.md
       - SimplicityHL: getting-started/simplicityhl.md
       - Rust: getting-started/rust.md
       - Haskell: getting-started/haskell.md