Tài liệu Halis

Halis là ngôn ngữ hệ thống an toàn, tự host, biên dịch native. Đây là tài liệu tham chiếu cho ngôn ngữ, hệ effect, thư viện chuẩn và toolchain.

Bắt đầu từ đâu

Nếu bạn muốn…	Đi tới
Chạy chương trình đầu tiên	Bắt đầu
Hiểu vì sao một hàm là thuần khiết	Effect
Xem dữ liệu không tin cậy được xử lý ra sao	Theo dõi taint
Tra một kiểu hay một phép chuyển đổi	Kiểu dữ liệu
Tra một effect, builtin hay target	Tra cứu nhanh
Theo dõi một bản phát hành	Các bản phát hành

Ba ý tưởng

Mọi thứ trong Halis đều bắt nguồn từ ba ý tưởng.

An toàn là mặc định, không phải lựa chọn. Tràn số nguyên, chia cho 0 và truy cập ngoài biên đều dừng an toàn. Không có công tắc nào tắt được các kiểm tra này — cách duy nhất một kiểm tra biến mất là một chứng minh hình thức rằng nó đã chết.

I/O là một effect, và effect phải được khai báo. Một hàm không có mệnh đề uses được trình biên dịch bảo đảm là thuần khiết — không phải theo quy ước, không phải sau khi review, mà do cấu trúc ngôn ngữ. Trình biên dịch đi đồ thị gọi và từ chối biên dịch một hàm đi tới một effect mà nó chưa khai.

Không gì bị giấu. Mọi giá trị mang kiểu khai báo tường minh, không có null, không có biến toàn cục, và hlc --audit in ra báo cáo capability và luồng taint của từng hàm trong chương trình.

Ngôn ngữ trong một tệp

import "std.sanitize"

struct Point {
    x: int,
    y: int
}

impl Point {
    fn dist2(self: Point) -> int {
        return self.x * self.x + self.y * self.y
    }
}

fn greet(name: str) -> str {
    return "Hello, " + name + "!"
}

fn main() -> int uses Args, IO {
    let p: Point = Point { x: 3, y: 4 }
    println("dist2 = " + p.dist2().to_str())
    println(greet("Halis"))

    # Dữ liệu từ dòng lệnh đến đã bị taint; làm sạch trước khi tới sink.
    let argv: list[tainted[str]] = tainted_args()
    if argv.len() > 1 {
        println("hello, " + sanitize_filename(argv.get(1)))
    }
    return 0
}

greet không có mệnh đề uses, nên trình biên dịch chứng minh nó thuần khiết: nó không thể in ra, không thể đọc tệp, không thể đọc đồng hồ và không thể chạm vào mạng. main khai Args và IO, và trả giá đúng cho hai thứ đó.

Đặc tả

Tài liệu chuẩn và có tính pháp lý là SPEC.md trong kho mã. Bề mặt API của v1.0 được ghim tại một digest cố định và hls-freeze từ chối mọi thay đổi lệch.

Lưu ý rằng SPEC.md là tài liệu lịch sử — nó mô tả ngôn ngữ như nó đã tiến hoá, qua từng stage. Ở những chỗ nó khác với trình biên dịch đã phát hành, trình biên dịch là đúng, và trang tra cứu nhanh được sinh từ mã nguồn của trình biên dịch.