From b08ee671d50f22632ce235fcb366df570475549b Mon Sep 17 00:00:00 2001 From: Dom Date: Mon, 22 Dec 2025 12:30:32 +0900 Subject: [PATCH] fixed some links, adjusted grammar, fixed some spelling mistakes. 1 comment --- .../common-programming-concepts.md | 2 +- src/foreword.md | 4 ++-- src/introduction.md | 6 +++--- src/title-page.md | 4 ++-- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/common-programming-concepts/common-programming-concepts.md b/src/common-programming-concepts/common-programming-concepts.md index 434a431..d77ea7a 100644 --- a/src/common-programming-concepts/common-programming-concepts.md +++ b/src/common-programming-concepts/common-programming-concepts.md @@ -4,4 +4,4 @@ This chapter covers common programming concepts that are shared across many prog In this chapter, we cover data types, functions, and comments. Understanding these concepts is essential for writing programs in Inference. -> Inference keywords, data types, and other language constructs are covered in the [Language Reference](../appendix/language-reference.md) appendix. +> Inference keywords, data types, and other language constructs are covered in the [Language Reference](../appendix/a-language-reference.md) appendix. diff --git a/src/foreword.md b/src/foreword.md index d86e141..1cbc537 100644 --- a/src/foreword.md +++ b/src/foreword.md @@ -2,8 +2,8 @@ Software correctness is a cornerstone of reliable computing systems. As humanity invents and develops more sophisticated and immersive technologies, the demand for resilient software that behaves exactly as intended has become increasingly critical. We have always had systems that must never fail because their real-world side effects are irreversible by nature. For example, nuclear power plant control software should never drain coolant from a reactor, and aircraft engines must not stop under any circumstances. -The Inference project started in January 2023 to address the challenges that this new era of computing brings. With the advent of blockchain and cryptographic protocols, quantum computing, AI-managed systems, and robotics, the need for software that is provably correct and secure has never been more pressing. No one wants a household robot to decide to iron already worn clothing. Likewise, blockchain smart contract exploits cause not only financial losses but also slow the evolution of the financial system, which is particularly harmful as of the end of 2025. +The Inference project started in January 2023 to address the challenges that this new era of computing brings. With the advent of blockchain and cryptographic protocols, quantum computing, AI-managed systems, and robotics, the need for software that is provably correct and secure has never been more pressing. No one wants a household robot to decide to iron clothes that are currently being worn by someone. Likewise, smart contract exploits do more than just drain funds, they hinder the evolution of financial systems. -Traditional testing and debugging methods, while useful, often fall short of providing absolute guarantees about program behavior. Formal Verification (FV), despite being one of the most advanced and reliable techniques for ensuring the correctness of algorithm implementations, has for decades been marginalized and used primarily in aerospace, military, and other safety-critical industries. +Traditional testing and debugging methods, while useful, often fall short of providing absolute guarantees about program behavior. Formal Verification (FV), despite being one of the most advanced and reliable techniques for ensuring the correctness of algorithm implementations, has for decades been underrepresented and used primarily in aerospace, military, and other safety-critical industries. >Inference aims to bring Formal Verification into the software engineering mainstream. diff --git a/src/introduction.md b/src/introduction.md index bb2592b..6a1e958 100644 --- a/src/introduction.md +++ b/src/introduction.md @@ -1,6 +1,6 @@ # Introduction -You are reading a book about _The Inference Programming Language_. With Inference, you can write highly reliable, mission-critical programs with a high level of confidence that they will behave exactly as intended. Inference is designed from the ground up to support formal verification (FV) of program properties, allowing you to prove code correctness mathematically — with machine-checked proofs of behavior — without needing to learn complex mathematical theories or specialized verification tools. Inference lets you write programs and their specifications in the same language and even in the same file, much like you would do with unit tests. +You are reading a book about _The Inference Programming Language_. With Inference, you can write highly reliable, mission-critical programs with a high level of confidence that they will behave exactly as intended. Inference is designed from the ground up to support formal verification (FV) of program properties, allowing you to prove code correctness mathematically with machine-checked proofs of behavior without needing to learn complex mathematical theories or specialized verification tools. Inference lets you write programs and their specifications in the same language and even in the same file, much like you would do with unit tests. ## Who Inference Is For @@ -8,7 +8,7 @@ The key power of Inference is that it has formal verification built-in from the ### Teams of Developers -Inference provides a way to rigorously ensure the correctness of code through formal verification. For development teams working on mission-critical applications, this means they can obtain mathematical guarantees that specified properties of their programs always hold, rather than relying solely on testing and code review. This leads to substantially lower residual defect risk, higher quality software, increased reliability, and improved users safety. +Inference provides a way to rigorously ensure the correctness of code through formal verification. For development teams working on mission-critical applications, this means they can obtain mathematical guarantees that specified properties of their programs always hold, rather than relying solely on testing and code review. This leads to substantially lower residual defect risk, higher quality software, increased reliability, and improved safety of its users. Examples of such software include, but are not limited to: - Cryptographic software and security systems @@ -20,7 +20,7 @@ Examples of such software include, but are not limited to: ### Researchers -Traditionally, formal verification has been a complex and specialized field, requiring deep knowledge of mathematical theories and specialized tools. Most of the existing formal verification tools are used by experts from academia and research institutions. Inference lowers the barrier to entry for researchers and provides a unified platform for writing and verifying code, making it easier to explore new ideas and push the boundaries of what is possible with formal verification. +Traditionally, formal verification has been a complex and specialized field, requiring deep knowledge of mathematical theories and specialized tools. Most of the existing formal verification tools are used by experts from academia and research institutions. Inference lowers the barrier of entry for researchers and provides a unified platform for writing and verifying code, making it easier to explore new ideas and push the boundaries of what is possible with formal verification. ### Students diff --git a/src/title-page.md b/src/title-page.md index a22bfd4..8212f2a 100644 --- a/src/title-page.md +++ b/src/title-page.md @@ -1,8 +1,8 @@ # The Inference Programming Language > [!WARNING] -> The Inference programming languge is currently under development. If you see this message, it means that the first stable release is not yet out. However, this books describes the current state of the language and currently available features. Therefore, feel free to explore and try out Inference! +> The Inference programming language is currently under development. If you see this message, it means that the first stable release is not out yet. However, this book describes the current state of the language and currently available features. Therefore, feel free to explore and try out Inference! To follow updates about the language and its development, follow the dev team official social media channels [](https://github.com/inferara)・[](https://x.com/inferara_kk)・[](https://discord.gg/NgWfmnmS5C)・[](https://inferara.com) ->We welcome contributions from the community. You can help improve Inference by trying out the language and sharing your experience, providing [feedback](https://github.com/Inferara/inference-language-spec/issues) on language features and design decisions, [reporting](https://github.com/Inferara/inference/issues) implementatoin bugs, suggesting [improvements](https://github.com/inferara/book/issues) to this documentation, or discussing new features on our [Discord](https://discord.gg/NgWfmnmS5C). Your input helps shape the development of Inference. +>We welcome contributions from the community. You can help improve Inference by trying out the language and sharing your experience, providing [feedback](https://github.com/Inferara/inference-language-spec/issues) on language features and design decisions, [reporting](https://github.com/Inferara/inference/issues) implementation bugs, suggesting [improvements](https://github.com/inferara/book/issues) to this documentation, or discussing new features on our [Discord](https://discord.gg/NgWfmnmS5C). Your input helps shape the development of Inference.