Bỏ qua, tới nội dung chính
Halis
v1.0.1
v1.0.1MIT9 effect0 GCtự host

An toàn là mặc định.

Effect phải được khai báo. Mọi phép toán đều được kiểm tra. Không gì bị giấu.

Halis là ngôn ngữ hệ thống an toàn, tự host, biên dịch trước ra mã máy. 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ữ.

Chỉ cần một shell và curl. Không cần toolchain biên dịch, không cần Python.

examples/effects_demo.hls HLS
fn read_config(path: str) -> str uses Fs {
    return read_file(path)
}

fn elapsed_ms() -> int uses Clock {
    return clock_ms()
}

fn pure_compute(n: int) -> int {
    # No uses clause -> pure by default
    let mut s: int = 0
    let mut i: int = 0
    while i < n {
        s = s + i
        i = i + 1
    }
    return s
}

fn main() -> int uses IO {
    let n: int = pure_compute(10)
    println("sum(0..10) = " + n.to_str())
    return 0
}
❯ $ hlc --audit examples/effects_demo.hls
hàm khai báo tính toán
-------------- ---------------------- ------
pure_compute (none - pure) (none)
read_config Fs Fs
elapsed_ms Clock Clock
program_args Args Args
main IO, Fs, Clock, Args, Exit IO, Fs, Clock, Args, Exit
kết luận: ĐẠT
Capability đã khai báo so với những gì trình biên dịch tự tính ra khi đi đồ thị gọi. Đọc mô hình effect đầy đủ →
Các bảo đảm

Bảy bảo đảm. Bảy điều bạn không còn phải nhớ.

Mỗi bảo đảm dưới đây được ghim vào một sổ cái kiểm chứng bằng máy. Phạm vi tài liệu thưởng bug-bounty cũng chính là sổ cái đó.

01

I/O là một effect được khai báo

Chín effect — IO, Fs, Clock, Args, Exit, Net, Rand, Proc, Conc — được khai trên chính hàm cần chúng và được kiểm tra xuyên suốt đồ thị gọi. Không có đường thoát nào qua lời gọi gián tiếp.

02

Mọi thao tác đều được kiểm tra

Tràn số nguyên, chia cho 0, truy cập ngoài biên — tất cả 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.

03

Không null. Không gì ẩn

Không null, không trạng thái chưa khởi tạo, không biến toàn cục, không ẩn giấu. Tất cả đều tường minh để có thể kiểm toán từng dòng.

04

An toàn bộ nhớ mà không cần GC

Dùng-sau-move là lỗi biên dịch; clone() sao chép sâu; runtime giải phóng đúng tại lúc thoát khối. Bộ kiểm tra căng thẳng bộ nhớ chạy hàng trăm nghìn vòng cấp phát với RSS phẳng, dưới giới hạn 256 MB không gian địa chỉ.

05

Race dữ liệu bất khả thi theo cấu trúc

Giá trị chỉ đi qua ranh giới task bằng kênh; chia sẻ một biến với một task ngoài kênh là lỗi biên dịch. Ngôn ngữ không có lock nào — đó là mô hình actor.

06

Dữ liệu không tin cậy bị taint mặc định

Giá trị tainted[T] không thể tới sink — in ra, tệp, thoát chương trình, DNS, tiến trình con — cho tới khi đi qua std.sanitize hoặc một lệnh untaint tường minh.

07

Toàn bộ chương trình đều kiểm toán được

hlc --audit in báo cáo capability và luồng taint của từng hàm: khai báo so với tính toán, và gọi tên vi phạm nếu có.

Hệ effect

Chín effect, khai báo đúng chỗ cần.

Một hàm nói rõ nó cần những capability nào. Những gì nó không nói thì nó không thể làm. Trình biên dịch kiểm tra điều đó xuyên suốt đồ thị gọi — không có đường thoát nào qua lời gọi gián tiếp.

Effect Nhóm Builtin Sink taint
IO Vào / ra print, println, read_line +6 print, println, eprint
Fs Vào / ra read_file, write_file, file_exists, read_file_tainted +8 read_file, write_file, file_exists
Clock Thời gian & ngẫu nhiên clock_ms, instant_now_ns, thread_sleep_ms +4 —
Args Vào / ra args, tainted_args +2 —
Exit Kết thúc exit +1 exit
Net Tiến trình & mạng net_lookup, net_tcp_connect, net_tls_get +11 net_lookup, net_tcp_connect
Rand Thời gian & ngẫu nhiên rand_int, rand_float, rand_seed +3 —
Proc Tiến trình & mạng proc_exec, env_get, cwd_get, sys_hostname +16 proc_exec
Conc Đồng thời chan_new, spawn, select, task.join, thread_yield +31 —

Danh sách effect và builtin được sinh tự động từ mã nguồn trình biên dịch (src/hlc/parser.hls và src/hlc/checker.hls), không gõ tay. Tra cứu nhanh →

Điều ngôn ngữ nói

Ngôn ngữ nói đúng điều nó làm.

Không có uses nghĩa là thuần khiết — không phải vì quy ước, mà vì trình biên dịch chứng minh được. Xoá uses IO ở hàm cuối cùng và chương trình không biên dịch được. Đó không phải cảnh báo lint; đó là một bằng chứng.

struct Point {
    x: int,
    y: int
}

impl Point {
    fn dist2(self: Point) -> int {
        return self.x * self.x + self.y * self.y
    }
    fn translate(mut self: Point, dx: int) -> void {
        self.x = self.x + dx
    }
}

fn main() -> int uses IO {
    let p: Point = Point { x: 3, y: 4 }
    p.translate(1)
    println("dist2 = " + p.dist2().to_str())
    return 0
}

Ví dụ từ examples/ của repo halis-lang

let p: Point = Point { x: 3, y: 4 }
Kiểu luôn được khai báo tường minh. Không suy luận kiểu ẩn, không đổi kiểu ẩn.
fn translate(mut self: Point, …)
mut trên tham số cho phép gán lại binding bên trong hàm.
self.x * self.x
Phép nhân trên int được kiểm tra tràn: tràn thì dừng an toàn, không cuộn ngầm.
Tự host

Điểm cố định, được chứng minh trên mọi bản build.

Trình biên dịch được viết bằng Halis, nên nó phải biên dịch được chính nó — và phải cho ra đúng kết quả đó.

snapshot/hlc.c seed đã commit bin/hlc compiler native src/hlc.hls snapshot của compiler cc compiles phải tái tạo byte-for-byte

Điểm cố định, không phải lời hứa

Mọi bản build đều phải tái dựng đúng snapshot đã commit, byte for byte. Snapshot cũ hoặc bị sửa tay sẽ làm build fail ngay lập tức.

Hai lần ignition độc lập

`make snapshot-chain` chạy bootstrap hai lần, so từng bước byte-for-byte rồi in ra chain digest. `CC2=clang` chứng minh một compiler khác vẫn ra cùng byte.

Không Python trên đường sống

Không đường build, release hay snapshot nào đọc Python. Interpreter chỉ là công cụ phòng thí nghiệm cho bộ test vi sai.

Hệ sinh thái

Toàn bộ toolchain được viết bằng Halis.

Không phải "một compiler hỗ trợ Halis" — mà là Halis biên dịch Halis. Mỗi tính năng ngôn ngữ mới phải được dùng bên trong chính compiler trước khi nó được phát hành.

Toolchain

Mọi công cụ đều viết bằng Halis và tự biên dịch chính nó. (30 công cụ native)

Biên dịch & kiểm tra
hlchlfmthllinthlbindgenhls-spec-checkhlfront
Trình soạn thảo & gỡ lỗi
hls-lsphls-daphls-replhlservehls-wasm-pack
Kiểm thử & đo lường
hltesthls-benchhls-rthls-dethls-rsshls-perf
Chuỗi cung ứng & quản trị
hls-pkghls-sbomhls-signhls-tloghls-freezehls-guaranteehls-lts

Thư viện chuẩn

Module thuần HLS, chia theo ba họ ứng dụng mà Halis hứa hẹn từ ngày đầu. (64 std + 18 core)

Lõi 13
strmathfmtlistsetcollectionsbitsoptionresulthashregextemplatelog
Hệ thống 12
iofsenvprocessthreadsynctimestreamasyncarchiveuuidnet
Web 16
httphttp2http_routerhttp_serverwebsocketssecookiesessioncsrfgraphqlopenapidomjsffijsffi_callbackurlhtml
Dữ liệu 10
jsonjson_streamcsvconfigcryptosha1sha256base64hexsimd
CLI 8
clituicolorprogresscompletemanhlsdochlscli
Bảo mật 2
taintsanitize
Kiểm thử 3
testquickcheckbench
Bare metal 18
core.alloccore.asmcore.atomicscore.bootcore.clonecore.dmacore.eqcore.interruptcore.itercore.memcore.mmiocore.optioncore.paniccore.portcore.resultcore.rtcore.sectioncore.stack
Target

Một ngôn ngữ, bốn kiểu đích.

Cùng một cây mã nguồn: biên dịch ra C rồi ra máy native, xuất LLVM IR, đóng gói WebAssembly, hoặc xuất một image bare-metal. Halis không xây hệ điều hành — Halis xây ngôn ngữ để viết hệ điều hành.

Native C x86_64 / aarch64 / riscv64 — Linux, macOS, Windows, FreeBSD. Đường biên dịch mặc định: AOT qua trình biên dịch C của hệ thống.
LLVM IR Phát xuất văn bản cho bất kỳ đích nào LLVM hỗ trợ.
WebAssembly wasm32 với std.jsffi và std.dom, tối ưu và đóng gói bởi hls-wasm-pack.
Bare metal x86_64 / aarch64 / riscv64 -unknown-none — Multiboot2/Limine, cú pháp IDT/GDT, MMIO, buffer an toàn DMA, script liên kết tuỳ biến, DWARF 5.
#![freestanding]#![no_std]kiểm soát bộ nhớ ở mức trangI/O khả biến (volatile)
Kiểm chứng

Bằng chứng, không lời tuyên bố.

Các bảo đảm ở trên không phải bài viết marketing — chúng là các hàng trong sổ cái soundness, mỗi hàng có cơ chế thực thi, điểm neo trong cây mã nguồn và các probe âm tính phải thất bại đúng như mong đợi.

15 dòng sổ cái soundness mỗi dòng có cơ chế và probe âm tính
9 effect tĩnh từ parser.hls và checker.hls
82 module thư viện chuẩn 64 std + 18 core
247 probe âm tính trong tests/fail/

Mỗi dòng sổ cái có cơ chế thực thi, điểm neo trong cây mã nguồn và các probe âm tính phải thất bại đúng như mong đợi. Phạm vi của tài liệu thưởng bug-bounty chính là sổ cái đó.

Snapshot C đã commit: 43,610 dòng, sha256 5943322a69d3ee1c…

G-MEM-01 · G-MEM-02 · G-TYPE-01 · G-ARITH-01 · G-EFF-01 · G-TAINT-01 · G-CONC-01 · G-MATCH-01 · G-CAP-01 · G-SBX-01 · G-CT-01 · G-FFI-01 · G-SPEC-01 · G-DET-01 · G-CORPUS-01

Câu hỏi

Câu trả lời thẳng thắn.

Những câu hỏi người ta thực sự đặt ra về một ngôn ngữ còn trẻ.

Halis có closure không?

Không. Có closure thì spawn sẽ phải bắt biến theo ngữ cảnh, và luật "chỉ truyền qua kênh" mới trở thành luật kiểm chứng được tĩnh. Việc thiếu closure là hệ quả có chủ ý của luật an toàn dữ liệu.

Taint tracking có chống được SQL injection không?

Chống được việc dữ liệu chưa được làm sạch chạm vào sink. Nó là một nhãn đơn: tainted[str, Html] và tainted[str, Sql] là việc chưa làm. Hôm nay, một lần sanitize xoá nhãn cho mọi sink.

Dùng được với C không?

Có, extern "C" có kiểm tra ABI. Nhưng header là thứ được tin: khai sai (khai int cho hàm trả char*) sẽ không bị phát hiện. hlbindgen giảm thiểu bằng cách sinh khối extern từ header kèm kiểm tra kích thước ABI.

Hiệu năng so với Rust và C ra sao?

Halis biên dịch AOT qua C, không có VM, không GC trong runtime. Chúng tôi không công bố benchmark so sánh cho tới khi có hạ tầng benchmark công khai; bốn dashboard hồi quy (perf, mem, ctime, size) theo dõi từng commit để phát hiện trượt.

Ai bảo trì dự án?

Một người duy nhất, giấy phép MIT. Nhánh main được bảo vệ, mọi thay đổi đi qua pull request với CI xanh.

Bản phát hành nào ổn định?

v1.0.1 là bản ổn định hiện tại. Dòng release/1.0 là dòng LTS: 3 năm sửa lỗi và 5 năm bảo mật, tính từ ngày cắt bản gốc của dòng.

Bắt đầu

Cài Halis trong một lệnh.

Không biên dịch gì cả. Mỗi archive phát hành mang theo toàn bộ toolchain — compiler và formatter dạng binary, thư viện chuẩn dạng mã nguồn — nên cài Halis là tải về, kiểm tra checksum, rồi chép vào chỗ.

curl -fsSL https://raw.githubusercontent.com/mhieuhonda/halis-lang/main/install.sh | sh
Kiểm tra SHA-256 so với SHA256SUMS của chính release trước khi giải nén bất cứ thứ gì.
Trình cài đặt tự chạy acceptance gate: biên dịch một chương trình std.result và format nó hai lần — lần hai phải bằng lần một.
--uninstall chỉ xoá đúng những gì bản ghi cài đặt đã tạo, không gì hơn.