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.
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.
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
}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 đó.
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.
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.
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.
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ỉ.
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.
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.
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ó.
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 →
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
}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 {
# Không có `uses` -> thuần khiết theo cấu trúc.
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
}import "std.sanitize"
fn main() -> int uses Args, IO {
# Mọi argv đến tay chương trình đều bị taint mặc định.
let argv: list[tainted[str]] = tainted_args()
if argv.len() > 1 {
# println là một sink: dữ liệu tainted không thể tới đó.
println("hello, " + sanitize_filename(argv.get(1)))
}
return 0
}fn fib(n: int) -> int {
if n < 2 {
return n
}
return fib(n - 1) + fib(n - 2)
}
fn worker(job: int, req: Chan[int], rep: Chan[int]) -> int uses Conc {
let answer: int = fib(job)
rep.send(answer)
return req.recv()
}
fn main() -> int uses IO, Conc {
let t: Task[int] = spawn(fib, 25)
let r: int = t.join()
println("fib(25) = " + r.to_str())
let req: Chan[int] = chan_new()
let rep: Chan[int] = chan_new()
let w: Task[int] = spawn(worker, 20, clone(req), clone(rep))
req.send(0)
let answer: int = rep.recv()
return 0
}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ả đó.
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.
`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 đườ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.
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.
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)
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)
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. |
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.
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
Những câu hỏi người ta thực sự đặt ra về một ngôn ngữ còn trẻ.
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.
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.
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.
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.
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.
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.
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ỗ.
SHA256SUMS của chính release trước khi giải nén bất cứ thứ gì. 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.