SKILL.md

Static Python

A subset of Python that transpiles to compiled languages.

Rules

• Use fixed-width integers: i32, u64, etc.
• Use decorators and composition instead of inheritance
• Use Result[T, E] instead of exceptions
• Use match as an expression. Note that there is no case keyword.

  match x:
      1: ...
      2: ...
  

• match can be nested inside other matches to write succinct code
• Elide types when easily inferred
• Always specify return types on functions
• Use design by contract with CHECKER.pre and CHECKER.post (from py2many.spec)
• Verify with either backend: theorem provers (Lean) or SMT solvers (z3)

Example

from py2many.spec import CHECKER

def classify_triangle(a: int, b: int, c: int) -> TriangleType:
    if CHECKER.pre:
        a > 0 and b > 0 and c > 0
        a < (b + c) and b < (a + c) and c < (a + b)

    if a == b == c:
        result = TriangleType.EQUILATERAL
    elif a == b or b == c or a == c:
        result = TriangleType.ISOSCELES
    else:
        result = TriangleType.SCALENE

    if CHECKER.post:
        result in (TriangleType.EQUILATERAL, TriangleType.ISOSCELES, TriangleType.SCALENE)

    return result

Reference

Unsupported features Verification Decorators