Safer Code with LLMs: Scala Types Silver Bullet?
summary
Claim: invoking Scala type system features in prompts makes LLM-generated code measurably safer. Methods: prompt experiments with open models (Llama 70B, Code Llama, Qwen, Gemma), verification via Stainless verifier, attention-map probing and tests derived from a 2021 vulnerability paper. Results: models show reduced safety issues but not perfect functional correctness; attention maps show type tokens drive real code changes while generic “safe” words do not. Prototype TypePilot generates well-typed Scala that, when it compiles, is usually secure for most models.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:47ML basics for functional programmers
- 6:16LLM limits in mainstream languages
- 9:25Security risks and hallucinations
- 13:18Human cost of unsafe AI coding
- 15:05Formal verification as safety
- 17:06Testing LLMs with Stainless
- 18:37Scala types for safer code
- 21:27Introducing TypePilot
- 23:35Debugging open vs closed models
- 25:21Agentic AI rise and risks
- 28:54Why Scala for safer agentic code
- 32:07Q&A
related talks
40mSafe Coding with LLMs - Verifiable Scala Silver Bullet
36mPrompting Safely: Building Secure LLM Prompts with a Scala DSL
01h 00mAI Safety through Programming?
29mLearning Scalaz
47mHarnessing LLMs for Next-Level Security Analysis
33mVerifiably Safe Agentic Compute
45mTypelevel Programming 101: The Subspace of Scala
18mScalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type(…)